{"entities":{"Q2926644":{"pageid":2937364,"ns":120,"title":"Item:Q2926644","lastrevid":52122314,"modified":"2026-01-20T23:51:12Z","type":"item","id":"Q2926644","labels":{"en":{"language":"en","value":"SMT-based array invariant generation"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6363633"}},"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":"Q2926644$3A6CD4D0-2785-449C-853C-9DBD23EF0717","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"be63863cda6f14d95456a7b2683709825bd2222c","datavalue":{"value":{"text":"SMT-Based Array Invariant Generation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2926644$FFD6EB00-2138-49B5-BAA7-F01546A07B2D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a2324a4ee1b9772a50be04f73d6994714683b30a","datavalue":{"value":"1426.68056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926644$515C1340-7923-45BC-A2AC-D1CB7E56AAA5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f8e119c61c7e3470a63f8186ed62025db03888a6","datavalue":{"value":"10.1007/978-3-642-35873-9_12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926644$D07F3A0D-1F33-49E4-926D-052365DCE1D6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"160bfe26a870f8433f093ce131383f68458dfba4","datavalue":{"value":{"entity-type":"item","numeric-id":2096442,"id":"Q2096442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2926644$B6BB12C7-2B89-4E0E-BB6F-38F6C8EFF32F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f1c6f3313098f94ac950042b92865f2f95306b33","datavalue":{"value":{"entity-type":"item","numeric-id":438575,"id":"Q438575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2926644$18824F27-FBE8-4ECB-B80E-5C70116C82AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"076f42ceb107ac95ece0987fd254ab37feda8487","datavalue":{"value":{"entity-type":"item","numeric-id":352976,"id":"Q352976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2926644$CF75C157-51F5-48CF-8DBC-6E3C5F984ECB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2926644$D00A13DA-63B3-4665-A10E-1D97BE1997F4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3daa83eb5c9d67846bd0433e54bd3c467e1d5cf9","datavalue":{"value":{"time":"+2014-11-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2926644$5B9A4920-C941-40BF-9490-55B9EB285AA3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926644$14120727-6079-44BC-A9F2-81F4966C8153","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"891e4014c51537aa18df5bcf797d9b603ed07335","datavalue":{"value":"6363633","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926644$3394DC82-267B-41A5-8224-4472733FA357","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a2b746efc66121bc1fb497da4ab39b83b5cd2f4c","datavalue":{"value":"program correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q2926644$DE6FCC33-82F4-44BC-A5AE-2F65657E43A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e4824208d7bba949dd72987d32ffb13493eeb0e","datavalue":{"value":"invariant generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2926644$8222342C-3A76-4125-B95B-8A29D0AFAF26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q2926644$A832FC6D-BFB9-4FA8-8C73-59759705593F","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":"Q2926644$142130C6-B7AF-43CB-A27F-94BC53A3A762","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"147d33351460fc464d043997b04166b7cf3253cb","datavalue":{"value":"https://doi.org/10.1007/978-3-642-35873-9_12","type":"string"},"datatype":"url"},"type":"statement","id":"Q2926644$60D817AA-7D8A-4B43-B52B-090B65D255A3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"286901c3cfb85b9f109c71e80ca268b8191b6b57","datavalue":{"value":"W71055133","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926644$A3C7587A-8178-44E3-99B7-DB46EA5CB47B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc47d371be75bc56a3d19a2e60b717b0a46b1228","datavalue":{"value":{"entity-type":"item","numeric-id":5900703,"id":"Q5900703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5b5eb140a1b5a7edd20b1bd4235dd4243b6267b","datavalue":{"value":{"amount":"+0.7956349849700928","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":"Q2926644$84E33C26-494B-4589-83E5-86684EDF965B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edbb0304e940bceb5735c561adfb0e7f12a33f27","datavalue":{"value":{"entity-type":"item","numeric-id":3646570,"id":"Q3646570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfb68e682daffdb6e8d296299004a1c2a63f1d74","datavalue":{"value":{"amount":"+0.7795675992965698","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":"Q2926644$7D7A2471-E8BD-434A-929D-843E7DB53022","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9113cabfcc806e4f1ce08e809a04d40e8ebf5d43","datavalue":{"value":{"entity-type":"item","numeric-id":4933316,"id":"Q4933316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0181d0f5103a2e4aa800b2e91ec43b5a9945ae87","datavalue":{"value":{"amount":"+0.7774420380592346","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":"Q2926644$C41FC27E-FBC7-41AD-A79B-5C29D2514DE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd18d3cac23c09596baa20c6cbc8879b4e8ac7bb","datavalue":{"value":{"entity-type":"item","numeric-id":4647830,"id":"Q4647830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f4facf7ee9608193bf997c0031417922f3eb288","datavalue":{"value":{"amount":"+0.7635790109634399","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":"Q2926644$EDDDF1FC-CFA9-46CC-9E60-E1BCBCFE2EC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ecf08f9e6eae6c33e54be636f8491d559294d6d6","datavalue":{"value":{"entity-type":"item","numeric-id":3004678,"id":"Q3004678"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7daa889bc29d0321b600a7983a15f9522a4aa6a4","datavalue":{"value":{"amount":"+0.7620229125022888","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":"Q2926644$4A51B33B-FB2C-4672-9305-074EE050E9F9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2926644","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2926644"}}}}}