{"entities":{"Q549686":{"pageid":551453,"ns":120,"title":"Item:Q549686","lastrevid":51292796,"modified":"2026-01-17T15:32:00Z","type":"item","id":"Q549686","labels":{"en":{"language":"en","value":"Predicate abstraction in a program logic calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5925512"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$A392AEB3-71CD-4133-AA15-244D1B48ACAB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fbf4c2f30a337bb7096abb46d0cfb5e07b95ded1","datavalue":{"value":{"text":"Predicate abstraction in a program logic calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q549686$CFFD54EA-AF93-4729-9F70-7DFACE56071B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"067c04bbeb2e54c838a39c8e3b3c443e3afb9165","datavalue":{"value":"1221.68066","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q549686$85ECE9D9-8C52-4B8E-846C-DA490859AE26","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"aaac08e9d7718d3fa6ca9f20924a3d2f73a26d2b","datavalue":{"value":{"entity-type":"item","numeric-id":549685,"id":"Q549685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$48D2C0F3-92C0-41D5-A6CF-E30CD48639C6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4082512e7d3530b9726df691c7c28e9fec542a8c","datavalue":{"value":{"entity-type":"item","numeric-id":169675,"id":"Q169675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$42D5A534-DE04-4640-95A5-B4DE319D97F2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3dd288f91e249ba649089623a2b7d89908afe78c","datavalue":{"value":{"time":"+2011-07-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q549686$3F72FFB8-D75D-4906-9FAA-045D5B14B97F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q549686$86ECD594-F61D-4841-895D-C37A5032EB1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q549686$E41959F3-F4F7-487B-B981-F4BC28975F5E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a55e9ba1898d0ccb0276ebac56331fab9de33aa6","datavalue":{"value":"5925512","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q549686$DD1997E3-7488-4E9D-A490-D257FE9C7056","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f02f4db7bd17ba3fbae1be6bcee13dc9e5aa86bc","datavalue":{"value":"formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q549686$A73172DB-5C03-492F-ACAD-16272A8CF5E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff93fcab863d9a2d7b61f398ca8507531735efa","datavalue":{"value":"software verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q549686$24D9782C-5313-4AAF-913A-8C9B5784F3B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q549686$0EEECB70-A692-4E7F-9BD6-8958BD23B8B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e4824208d7bba949dd72987d32ffb13493eeb0e","datavalue":{"value":"invariant generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q549686$577AEE59-6365-4B7E-B99F-893F48998D8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"271b051f29cb2edbed99f6c31256721127b7519f","datavalue":{"value":"abstract interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q549686$458B7A7D-33D4-4985-8995-CB0C5A1EA20C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9fb50508d9ae1a4b5b2525656ffbf4223c07463","datavalue":{"value":"predicate abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q549686$06BC587A-19FF-4BCE-8B1D-7CBEF4F53E4F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a7aa47621b17d0cd88eea4f1397181a4d6b8f672","datavalue":{"value":{"entity-type":"item","numeric-id":22029,"id":"Q22029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$0E2CD364-5850-4F9F-9521-5886C78CB7CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$D4460F7B-6FCD-49A9-8E18-C90D300E2092","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ea1fa890b2f09c8cd0bccb17957cf46696afec2a","datavalue":{"value":{"entity-type":"item","numeric-id":19731,"id":"Q19731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$EE17D29A-E0BB-416C-8F7A-6E3922796572","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"beb205139d0971fca32ffa61e5b55aaac31a7181","datavalue":{"value":{"entity-type":"item","numeric-id":16768,"id":"Q16768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$10164EEE-81DA-4002-9E79-C8E37514AEE4","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$7C5DC143-F4B0-407C-AEC6-3969E0265CB6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"375e6b301be94a20976d333b8c92682a3c5dafb0","datavalue":{"value":"https://doi.org/10.1016/j.scico.2010.06.008","type":"string"},"datatype":"url"},"type":"statement","id":"Q549686$D6FCBE56-49FB-408E-94EF-0E9ED94A4389","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e5ec24a33571b77552e06efdb5c8b69a74b3b413","datavalue":{"value":"W2142528518","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q549686$2A4BC2C5-A111-475B-A6D6-14B2950A5B52","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"890aa582ec37803cbf74c8a6ca1c70024ea8a626","datavalue":{"value":{"entity-type":"item","numeric-id":4012706,"id":"Q4012706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$26E9EDFF-A9CC-4D3F-9810-772699261B49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf1da1b48aad7248192eb6bac6e3c0872fcb00b8","datavalue":{"value":{"entity-type":"item","numeric-id":5178906,"id":"Q5178906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$40A82E7F-DDDF-4C7B-A9E9-46252C460782","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7cd2a25d693a4acd921e56f15d1b3d06cb750f8","datavalue":{"value":{"entity-type":"item","numeric-id":2754081,"id":"Q2754081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$96F425AE-AAD9-46B9-84E0-15C8C71B48D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65743db030291e7ba33e4a4ada75694a0e3c4b21","datavalue":{"value":{"entity-type":"item","numeric-id":3605465,"id":"Q3605465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$C5CE6ED7-2D23-4753-9D32-07542DA1D401","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e5ccf0b70a10206d3060a0ecdfcb0df27797b2d","datavalue":{"value":{"entity-type":"item","numeric-id":5493379,"id":"Q5493379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$765ED308-17EF-48AA-A062-11636E5E1584","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82ab6e8e0bdc75b20da172ab4510ad41a1c82a0e","datavalue":{"value":{"entity-type":"item","numeric-id":3608771,"id":"Q3608771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$8623F2D0-8EDE-46D7-B42B-4F7850F7BCD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2790188d3a2572a99d3b8280868598d27c040965","datavalue":{"value":{"entity-type":"item","numeric-id":4525781,"id":"Q4525781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$6D05557B-986F-4A7F-B274-27A9639F9CE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$BC877EF9-C534-4718-A263-15000B6B979B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cdc7283fe176cc7266c2ab2cb14158c061aab4a","datavalue":{"value":{"entity-type":"item","numeric-id":3613414,"id":"Q3613414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$CEC6673F-330C-4EDA-A483-D54FF8070D4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9b6bedea1cffabec2896430aabcdd08d9b551a1","datavalue":{"value":{"entity-type":"item","numeric-id":5387908,"id":"Q5387908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$C0831196-E2DC-4C08-A288-65D882F4DF4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83fa1aea41b23b77e49c2e6c48c1b67f2ce6b255","datavalue":{"value":{"entity-type":"item","numeric-id":4095837,"id":"Q4095837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$CCD1EBA4-11D4-4021-9FC4-768CB1A625C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f7228d911878a16429788a7e2e2b8ecaf57db22","datavalue":{"value":{"entity-type":"item","numeric-id":4817541,"id":"Q4817541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$A2698945-3E1F-4315-8AF6-04CCAC5F4319","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$C08F4902-57CB-4FFC-9112-B7BADFED7EEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a2f60f551f2414de9c53ee958f83542a8b6793d","datavalue":{"value":{"entity-type":"item","numeric-id":5466565,"id":"Q5466565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q549686$CC206156-C19E-4890-AE56-0E38A495B0B2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"885ef2101684cc65bfa64174803183ab545f92e2","datavalue":{"value":"10.1016/J.SCICO.2010.06.008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q549686$7CEE5A73-C2BD-4C71-ACDE-B39007044824","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a06955dffd6e327f4d11c4c479c99ae3ef1bd848","datavalue":{"value":{"entity-type":"item","numeric-id":3605465,"id":"Q3605465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06897702b020914a75f256c565b51c8f594e4b3d","datavalue":{"value":{"amount":"+0.9923221468925476","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q549686$FBF559ED-6325-4D20-9CB0-99EE253E1EF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"79ffa5ff30461cd51e0211fecdb41174f0327193","datavalue":{"value":{"entity-type":"item","numeric-id":5897055,"id":"Q5897055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ccc663542ff4bec2c14ae7afdb68a5556e875ce","datavalue":{"value":{"amount":"+0.8188765645027161","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q549686$9ACCAA21-9CD0-4B23-8948-626F83EC8DD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dadf15a86ab27de24c71c6278f501043afe2c895","datavalue":{"value":{"entity-type":"item","numeric-id":5277793,"id":"Q5277793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a61938bfcee42b0b1963c513482b868fb7f33813","datavalue":{"value":{"amount":"+0.8050113320350647","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q549686$D88378E0-AA06-4E42-9215-5BADEA89F013","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b400ee7dab70c859b6f84076d6aeedebe112d4db","datavalue":{"value":{"entity-type":"item","numeric-id":1888196,"id":"Q1888196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"968602454947ec0434a655530b6e1b85036ef66f","datavalue":{"value":{"amount":"+0.8011196851730347","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q549686$D2DD655D-C6DA-4D0B-AE4D-4BEC985DAAD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7bac9d4d28f254e49858c9874367df8c34d82c78","datavalue":{"value":{"entity-type":"item","numeric-id":3176373,"id":"Q3176373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd4179de4ae957ea8e06098b34e6e630a8fea899","datavalue":{"value":{"amount":"+0.7811768054962158","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q549686$31E19585-4808-42D3-8272-49815AE36F41","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:549686","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:549686"}}}}}