{"entities":{"Q5408554":{"pageid":7438128,"ns":120,"title":"Item:Q5408554","lastrevid":51972545,"modified":"2026-01-20T16:11:40Z","type":"item","id":"Q5408554","labels":{"en":{"language":"en","value":"Predicate abstraction and refinement for verifying multi-threaded programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6282615"}},"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":"Q5408554$7D664C13-B3A3-4956-8992-3ED85E58DF84","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"95d0ce3f1827ca03fa3e270d53654c0d74fe7e3f","datavalue":{"value":{"text":"Predicate abstraction and refinement for verifying multi-threaded programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5408554$BE14B708-51E3-4284-9679-E9B1D99239CC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c60e7f2a697d33a6c9399de4a922113e00da8233","datavalue":{"value":"1284.68427","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408554$56B807E3-B2BC-4437-B5A8-3F99F4934B4B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"503dff56407320bc68d6e52bdfa036bbdc30c1fb","datavalue":{"value":"10.1145/1926385.1926424","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408554$C25A8724-E5EA-4919-A98D-A6C1F478D252","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cefe2994cd2e378e79e344a451c126379a495f1d","datavalue":{"value":{"entity-type":"item","numeric-id":630709,"id":"Q630709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408554$0CAD686F-C348-4D4A-BB19-3553DA6F8BA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"33f09e7b1eefa8c699a9d529da40fe033eb88541","datavalue":{"value":{"entity-type":"item","numeric-id":604393,"id":"Q604393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408554$D20BFF25-2105-4236-B0F6-BB4579025CFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eb5194b074431f4ab5210cd57ca7a7f1a1e79525","datavalue":{"value":{"entity-type":"item","numeric-id":948221,"id":"Q948221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408554$5BAABE65-E6D7-4A29-AE69-2617F10F58C1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"724e86f0a622186aef680198e4fbf5470f7a0c57","datavalue":{"value":{"entity-type":"item","numeric-id":5408524,"id":"Q5408524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408554$9DCE3E8E-E264-4F1F-BE3D-19764EB84140","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d29d162184913e14034b04455ad3f441d2a1856b","datavalue":{"value":{"time":"+2014-04-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5408554$DC9CF3E2-77AD-45E7-85E7-505CEECEB6F3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408554$138F2487-6642-4C3D-8A44-26060F90FF5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1908801a2431998085c7d582418a428f7e7f6658","datavalue":{"value":"68M20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408554$FB014ED7-6FCA-4EDB-AD46-B94A2B0FBDAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35c3f01235ccba091e1644bb05c86f53d45fd7f7","datavalue":{"value":"68N19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408554$D6AE2530-0EFF-4007-A419-AA43F8775C0D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"dcb20b0df263210f8ea2a76cc595c2985505ebba","datavalue":{"value":"6282615","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408554$A61110F4-EA10-4B4C-B542-A10732695DE2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f742b3cdd1b0a15c6b96e58001080b879ed46a4b","datavalue":{"value":"(transition) predicate abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408554$620C62BB-C601-4F19-982F-7EE46A3C0DDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9917a2dfd376250c18f9925b8d22d45575bb3eef","datavalue":{"value":"abstraction refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408554$4575943A-87F5-44C0-B515-2A0F9D5DBB32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d7d1aa3ae319733d3e20fe7888c7b88a225e7377","datavalue":{"value":"environment transitions","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408554$49EE1F0E-5CFD-482F-AB69-B618B7772F83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e431190495251d75e7d7f973ca704f4139885eb","datavalue":{"value":"Horn clauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408554$5CB15E12-3320-4382-AA8C-915F743B92E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff513d24e10502d41033b35d41538efbc83c1eee","datavalue":{"value":"modular reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408554$81D66FA8-3841-43EA-80E5-B70E099F5498","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"458c2b35d0451140b7681e6642905d2f8f38d563","datavalue":{"value":"multi-threaded programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408554$E39A9C5F-2E56-4207-BC5C-BD7C84A85FE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"edc54e2ee713bf6ef933abe433da86dc03aec7ba","datavalue":{"value":"proof rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408554$64417DDE-9818-48F1-AB49-4D0352B155D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d584e359576a00f85def0b98465ac7707c1c7959","datavalue":{"value":"safety","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408554$2DDA5C0B-F609-4A42-8CCB-824C22302010","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":"Q5408554$788A00C5-855D-4675-BC05-37045E3A1EF9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1390061f5432654e5ce091956b666387afc1a6c9","datavalue":{"value":"https://doi.org/10.1145/1926385.1926424","type":"string"},"datatype":"url"},"type":"statement","id":"Q5408554$C4FF12B6-EF58-464A-9BCF-7333C04BF0F5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"559aa260b34577815dd1a4016fdac469daf0f94a","datavalue":{"value":"W4236040576","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408554$A7F61BD1-5494-4BA4-BE00-06055D266ABB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4cd8fe519b64cbc856a832a8dd1f77f177c5e155","datavalue":{"value":{"entity-type":"item","numeric-id":3656886,"id":"Q3656886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e22579b68036e39e5140c45b771a8f30d52ac8dc","datavalue":{"value":{"amount":"+0.7795650959014893","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":"Q5408554$8B28C7C6-6469-4657-8295-5EBEAEDBBAB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85ebbee7b7abce6bc9db7943aebd0d1ded4c399e","datavalue":{"value":{"entity-type":"item","numeric-id":1888200,"id":"Q1888200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed8391c4c72e0d5ad4638ba35875fd89ca0ede5c","datavalue":{"value":{"amount":"+0.7553754448890686","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":"Q5408554$7ED887AC-A76C-4F58-8C30-5269F9D5728E","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":"c48b9cac2df178b6c5375eb2b5d102a7918558b6","datavalue":{"value":{"amount":"+0.7534520030021667","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":"Q5408554$0970F647-202E-4846-B00B-55861B42A9CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11529eb4ce409ad0cf813c2502fa801a2afa7f1a","datavalue":{"value":{"entity-type":"item","numeric-id":4931292,"id":"Q4931292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a6b2bf7d65cb0d8fd626ac49a98f636282c839f","datavalue":{"value":{"amount":"+0.7459954619407654","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":"Q5408554$FC61931D-8697-4E6B-B28E-31AC02630574","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ba55ee38a99d46604b9b2feddb9efbde5b9b1bb","datavalue":{"value":{"entity-type":"item","numeric-id":5240105,"id":"Q5240105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b827ddbc949e03bd62da0c77772789c09228a4ef","datavalue":{"value":{"amount":"+0.7423269748687744","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":"Q5408554$44B6C613-95D9-4140-9553-BD5A7D3A77D8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5408554","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5408554"}}}}}