{"entities":{"Q6488472":{"pageid":14067241,"ns":120,"title":"Item:Q6488472","lastrevid":47841685,"modified":"2026-01-02T20:40:35Z","type":"item","id":"Q6488472","labels":{"en":{"language":"en","value":"Trace Abstraction-Based Verification for Uninterpreted Programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7677001"}},"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":"Q6488472$73BB669E-C6E5-44F4-95B3-CC1BB3148245","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4bc2bb036b003f3b5c22e7fb8add88e1b746c0c0","datavalue":{"value":{"text":"Trace Abstraction-Based Verification for Uninterpreted Programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6488472$EC1B1C4F-95C8-4E59-9269-5D9C10C3D582","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e958263cbb2432c88145f8e7b18dff3b3abbb69e","datavalue":{"value":"1521.68078","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6488472$0B055A70-35FC-4233-B72A-B1DDD3E7EA9D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"66d62b56ad37a6f2526749efba2d804fd8cd46f3","datavalue":{"value":"10.1007/978-3-030-90870-6_29","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6488472$71E9A13C-5D01-4D74-9D35-3F504318A727","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6a567d2ee6f65c2b6b20ce40a79b36f311a95aa6","datavalue":{"value":{"entity-type":"item","numeric-id":4989715,"id":"Q4989715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$BA4C6D38-8BFE-4FD9-A3A3-008D9BE7C3D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"be944286afc345df75c2ec6bc9a42c95fc82cd58","datavalue":{"value":{"entity-type":"item","numeric-id":714876,"id":"Q714876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$CDE42E51-C027-466B-AAA7-538F57D027F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7aa871e45e43606569d61b3b9bdc1e07171d5c51","datavalue":{"value":{"entity-type":"item","numeric-id":6488471,"id":"Q6488471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$1CDE5EB2-7FEC-455B-B634-B20078DF2920","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a987699fd23888733c3cf6186ec5b68180cd27f8","datavalue":{"value":{"entity-type":"item","numeric-id":281290,"id":"Q281290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$FEDD2BE7-F886-44A5-8875-FB53532E57B5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"260332f705ad2e0d1275bea375e8ebc598a68071","datavalue":{"value":{"time":"+2023-04-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6488472$AA8C3CBF-75E8-4C05-BFCA-054ECBE27F85","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6488472$07EBA970-E21E-47F1-B7AD-3593A5E56B63","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e9a093226ec6503f773cd9e07d61456e10f302ea","datavalue":{"value":"7677001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6488472$7C4F7742-3494-4EDD-A25E-A642776A6AA8","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":"Q6488472$944D6753-26A4-4716-8885-35F28EC34727","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c21793cbba54b76515f61e513f7a3aba8da8e8ee","datavalue":{"value":{"entity-type":"item","numeric-id":4989166,"id":"Q4989166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$96370958-0D6F-4401-B268-F4782B7852AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"547ea93e9e2f717f44952d9eb38757244cbb564e","datavalue":{"value":{"entity-type":"item","numeric-id":3460058,"id":"Q3460058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$0FA16DFE-14A7-4DF1-A507-FFF34FB4A675","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":"Q6488472$B7B2A3DE-BAC7-4496-B761-06A331B41E4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acde43aadb68c83ae4d51574dcef8cc0958b2d7d","datavalue":{"value":{"entity-type":"item","numeric-id":3392921,"id":"Q3392921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$B631A491-2959-4260-B0E7-C4AB9329CD88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fcf2b678c67af5d9c3ef01ce8f5125a52e30717a","datavalue":{"value":{"entity-type":"item","numeric-id":5255103,"id":"Q5255103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$3954B76C-DA59-41FB-9FF2-6379AD02F56B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c91a28a758cef65772d101c4d9ed9dccc99d931","datavalue":{"value":{"entity-type":"item","numeric-id":2942878,"id":"Q2942878"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$8AC1F922-3B87-47BA-AB6E-C849B76E7612","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb53b69a005134b7aae07b4949b21bc26d9d6bca","datavalue":{"value":{"entity-type":"item","numeric-id":4344149,"id":"Q4344149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$94363621-49A4-458C-8FD1-6BBEBF230082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"702865848cb15e407debca29db0e1f097f9b86e4","datavalue":{"value":{"entity-type":"item","numeric-id":518892,"id":"Q518892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$0849BCFB-CD20-4EC4-8578-EC21F60ECFC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"091106aada8a83b8337d8fedb55405822e9d4c57","datavalue":{"value":{"entity-type":"item","numeric-id":2226763,"id":"Q2226763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$25E529D1-3167-42B8-8E67-7C7BE85C77C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1807204606c08bc0647f8c538053670a3e876b3b","datavalue":{"value":{"entity-type":"item","numeric-id":3066108,"id":"Q3066108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$22F5301B-5A09-4DB7-BCB9-3D0FAF229B81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eab20597048cbd154564fb07c83caf3de2fb98f9","datavalue":{"value":{"entity-type":"item","numeric-id":5164172,"id":"Q5164172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$FF4E53E4-0B72-459D-9DFF-D38BEE643BF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"975126c2667d6964e52988e556bf8223ff836bfd","datavalue":{"value":{"entity-type":"item","numeric-id":3883564,"id":"Q3883564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$A6AB083F-026E-436D-AB26-D7D4D673EC54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2c343dd01ae333921b2cfba22694c9ff234c138","datavalue":{"value":{"entity-type":"item","numeric-id":5875684,"id":"Q5875684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488472$CE9A5C0E-F8FA-4C0E-A950-DC14E04C3E4B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bed03ff244bd448296e984cc4bf4f360cb72a649","datavalue":{"value":{"entity-type":"item","numeric-id":4414376,"id":"Q4414376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac1c62e78834ed8aa4830d40362669f05fcf91a8","datavalue":{"value":{"amount":"+0.7480313181877136","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":"Q6488472$335BC7C1-A6F3-4F35-AA7F-474CD56A858A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d61904075969ef14dde390182fa67ccf6bbc6ba","datavalue":{"value":{"entity-type":"item","numeric-id":2281622,"id":"Q2281622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"12a2a88a760836a23dad025f5cb448e8661e92c9","datavalue":{"value":{"amount":"+0.7431220412254333","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":"Q6488472$DDCEE3AA-7A1A-4787-8DE9-BD8658ADB460","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1755c681f2850b9c2be50d8a3f34fae490a03b10","datavalue":{"value":{"entity-type":"item","numeric-id":479820,"id":"Q479820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9e083b4b3de4c1c6554c9390764fc53ae44d905","datavalue":{"value":{"amount":"+0.7376336455345154","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":"Q6488472$45D6944B-458D-40C8-A25F-EAE7DEF68EFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a3461117f43bb94ebdf7175fb5aa239d921e50d","datavalue":{"value":{"entity-type":"item","numeric-id":6045018,"id":"Q6045018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e55f6b931292864e2a63c2b206d5388002fa7120","datavalue":{"value":{"amount":"+0.7348966598510742","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":"Q6488472$F48A44FC-41CA-491E-BBC9-153CB158E64D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5cbe632a0b297f0680635d38f64812e52ca73f4a","datavalue":{"value":{"entity-type":"item","numeric-id":3392921,"id":"Q3392921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"03400975bb9e63b07457ec76f4b68c20b8f93de8","datavalue":{"value":{"amount":"+0.7332621216773987","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":"Q6488472$102782D5-21C3-458B-8D58-7001F2B09DB3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6488472","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6488472"}}}}}