{"entities":{"Q5255063":{"pageid":7284631,"ns":120,"title":"Item:Q5255063","lastrevid":91719662,"modified":"2026-06-04T23:53:48Z","type":"item","id":"Q5255063","labels":{"en":{"language":"en","value":"Program analysis via satisfiability modulo path programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6445085"}},"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":"Q5255063$5EC5CF51-D31F-4CAF-B048-BE6E8B564B3F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6d197b7c1d3d066618a19fec3cffd867d4bf6671","datavalue":{"value":{"text":"Program analysis via satisfiability modulo path programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5255063$F4113CD0-0C32-47F7-902E-B70DCB30D65F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"09c5ec45589d922803be4db5838790cc9d47675f","datavalue":{"value":"1312.68058","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255063$02938ED6-F34E-44C6-9544-75BFC6004044","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8c92c12ca39565a263a52c378b4fb8ba92acea0d","datavalue":{"value":"10.1145/1706299.1706309","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255063$1719740F-7727-41A7-B6A7-A3449183A942","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"90445a82981b6e7b2f2657e880bf9e7e26c8ddbb","datavalue":{"value":{"entity-type":"item","numeric-id":1696588,"id":"Q1696588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5255063$1932C88B-18CF-41E1-8BA2-EBFE33228A29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4d916c113e94bbfbdfe223618580740bb723d1be","datavalue":{"value":{"entity-type":"item","numeric-id":812049,"id":"Q812049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5255063$FBCC43B1-E0FC-4EC3-8F64-1106FBDABFBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"adf482bc390836e4c23988820629e51ba0628faa","datavalue":{"value":{"entity-type":"item","numeric-id":947792,"id":"Q947792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5255063$C4940E3B-7852-49C4-A43D-2FD58601F6E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"267769ee025773c3257f441a0558f5f2a60f51b9","datavalue":{"value":{"entity-type":"item","numeric-id":432145,"id":"Q432145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5255063$51A745C3-E8DB-43FF-BADC-5CA8073D1DAE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0a5bbee3666eee3a652778234a38c4005afc7cb6","datavalue":{"value":{"entity-type":"item","numeric-id":5255055,"id":"Q5255055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5255063$A7981219-BA2F-40BA-8A10-DD84236557E3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"00c841ea08739fa38b76821129fbbdb6fe48b753","datavalue":{"value":{"time":"+2015-06-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5255063$25E6C443-B086-4972-8A76-86A1D08C5D25","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0ef4bf9ea6bb65765581b76468e1e5a94321f9c4","datavalue":{"value":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.183.906","type":"string"},"datatype":"url"},"type":"statement","id":"Q5255063$A00BCC1A-3B3D-4FF1-9BE6-F5D9572387AD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255063$CD027319-8A73-45D0-AE2B-D78965B2CBE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255063$A3D0FF32-1262-423B-B1E3-5656969321C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255063$D1500F7E-C801-46DE-8250-36EC734380A0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"22a9275b181e7e70f764d991f9f60ef89018ee51","datavalue":{"value":"6445085","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255063$5DAF0B84-148B-4175-8815-834139595A96","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"271b051f29cb2edbed99f6c31256721127b7519f","datavalue":{"value":"abstract interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5255063$1FC2EB09-FF93-4AB6-B9A4-C16512641DC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9d3e6c3c46693ec1537d353b3f002b4bc52b6a29","datavalue":{"value":"path sensitivity","type":"string"},"datatype":"string"},"type":"statement","id":"Q5255063$7844028A-1832-447B-92FB-52F0E1A279B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0f668560f85d7afd1fece97b175bc3414226fbb","datavalue":{"value":"program analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q5255063$9E52B00D-E3F5-4B45-A65A-561FEEC7278A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"11e8fb24190d53185fc187965e543396cedadbb8","datavalue":{"value":"satisfiability solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q5255063$E277CFFF-FDFE-4834-A05E-F8BDD5C6BB85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"61439d791f6aac729372268f16b553bcf47e3b78","datavalue":{"value":"SMT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q5255063$F200B210-F63B-4B24-9613-0C1FE3ACF2A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69dd490da9b67dc4fe4c624a05791d0c4fa27f2e","datavalue":{"value":"symbolic execution","type":"string"},"datatype":"string"},"type":"statement","id":"Q5255063$34051989-8A8A-4380-8C68-A7A91BFA45C2","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":"Q5255063$ED4BCC05-C730-4E29-89E3-8239B54D8E0D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0e283dd66e5d0d035a93f2b4e07cb4c121b7dd7a","datavalue":{"value":"W2144789370","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255063$2B611BBF-ABBF-4492-A554-20356EE1FFDB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d066d72f00d33ed03ad9f01a76c02e766cf87c30","datavalue":{"value":{"entity-type":"item","numeric-id":5493391,"id":"Q5493391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f360e07d9bb035c337dcd876d62070697c2fad28","datavalue":{"value":{"amount":"+0.7123866677284241","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":"Q5255063$C62CB112-650A-484D-9479-6083FB1835AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66f94f667f06fe07b1d11319249f399c654cd26f","datavalue":{"value":{"entity-type":"item","numeric-id":3605478,"id":"Q3605478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"953000bcebc3a345e7204e4c6a72ae63f4defbcb","datavalue":{"value":{"amount":"+0.7097111940383911","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":"Q5255063$DF2F2D01-CA89-4E67-ADD5-AEF249780A4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7673030051fb16a992ddd4eef910d1493fa6145d","datavalue":{"value":{"entity-type":"item","numeric-id":5187836,"id":"Q5187836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64e791d0d073d04f63fde6e31c2c2fc4d752c038","datavalue":{"value":{"amount":"+0.6966876983642578","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":"Q5255063$CC9DBF8D-256F-41DE-B9D7-DA7949A7F558","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5068b654170e5aa67241c6b6ca566d7ac1ba362f","datavalue":{"value":{"entity-type":"item","numeric-id":3460902,"id":"Q3460902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a6ed79baa4bf4a61788240828fb3f2265a2d1f4","datavalue":{"value":{"amount":"+0.6953404545783997","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":"Q5255063$0BCEB83E-D0B7-46BE-9D66-2A836DFD857B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d368107344918cf344e91551289f3ea49aa9f173","datavalue":{"value":{"entity-type":"item","numeric-id":3189836,"id":"Q3189836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"979a944ed98b0eddb9de02addb117b006dc4a3e4","datavalue":{"value":{"amount":"+0.6953033804893494","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":"Q5255063$A2D47D47-F66E-4C15-9AA8-D91984AC4DCB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Program analysis via satisfiability modulo path programs","badges":[]}}}}}