{"entities":{"Q1656596":{"pageid":1667337,"ns":120,"title":"Item:Q1656596","lastrevid":68252385,"modified":"2026-04-12T22:28:07Z","type":"item","id":"Q1656596","labels":{"en":{"language":"en","value":"Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6916317"}},"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":"Q1656596$86749E0A-59E8-4C58-8CD4-23748FCA5F94","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"98c57664172c0b6521520c73841c388540968759","datavalue":{"value":{"text":"Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1656596$8DEBBDDF-861A-4F55-B052-F72F91635445","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6be0b2bc04b0018b96a6766862ade38e529a392d","datavalue":{"value":"10.1007/978-3-319-94144-8_22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1656596$B3C68604-DF60-43D2-B586-9E6007C43AFE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6b5ac3ca6091b50254e48fce55515cdec2a3e944","datavalue":{"value":{"entity-type":"item","numeric-id":1656592,"id":"Q1656592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$FB8A4BB5-F19E-4F42-88CA-993133AF6466","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"283edb0fb82934509dc8a47dcad25c94c0386a81","datavalue":{"value":{"entity-type":"item","numeric-id":1656593,"id":"Q1656593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$8F779E41-CF6E-417A-A6DB-A03BC89A3B48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4af60d03a1cfaaa22dec1b0f8a03e95f58573a2c","datavalue":{"value":{"entity-type":"item","numeric-id":1656594,"id":"Q1656594"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$D557C59C-414F-48CE-8885-03DB89FE72ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ee542ad0eead7e3864f23bc561740b3c8c3d3688","datavalue":{"value":{"entity-type":"item","numeric-id":1656595,"id":"Q1656595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$01331D63-CAD4-4493-B13B-B3D1E10A64BE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2dfbbfe69f220779a8f4ee2aa35287f4eb47a1e3","datavalue":{"value":{"time":"+2018-08-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":"Q1656596$9F08BAA8-DC3E-496D-9F30-5786DA1E4891","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1656596$3EB0568A-20A7-452C-8ADB-020C9DB2881F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1656596$5C9ABDD3-4A71-42CD-892B-518B31385AAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1656596$BAF12DA9-7271-45A3-BB86-C45BBC2FE281","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c9c62eb4d53d5021d5ff4151a374c99091b08f2c","datavalue":{"value":"6916317","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1656596$E3089DB6-E52A-444F-A18B-FD28F24BEF32","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6ffb7d804988b3c86a5855f78d1e0f2e36c4cad8","datavalue":{"value":{"entity-type":"item","numeric-id":12843,"id":"Q12843"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$78A4656F-DF4D-4C98-8E34-B2CD7EF37EFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$4CEE5D72-31DC-4D5C-AA1F-68492D82C2CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e435afb031ee44ca6c370c9a4082b74be3491e33","datavalue":{"value":{"entity-type":"item","numeric-id":16498,"id":"Q16498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$6DDD5308-5EC2-43DF-8B34-A0128298274F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$63F7B789-7288-4AA4-B82C-0687739E48CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$35EB3BFB-EF4C-4592-A948-E0928AC40AA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"176ca6df47c4f289ef4016b8f6a54a0a5756c45b","datavalue":{"value":{"entity-type":"item","numeric-id":14619,"id":"Q14619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$DE7BF8F5-FC49-44D8-8923-7E7BA700777E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d5dcb486ea2ffc39531287854f4a7be9ffb011b4","datavalue":{"value":{"entity-type":"item","numeric-id":17045,"id":"Q17045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1656596$20BE65F3-306A-4704-AC77-777548D2FC8B","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":"Q1656596$ABB671D2-8713-4B3F-BE1C-AE02E7A6A264","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8b70e6c84c88e569a93ad8ebff75b9bdca32552d","datavalue":{"value":"https://doi.org/10.1007/978-3-319-94144-8_22","type":"string"},"datatype":"url"},"type":"statement","id":"Q1656596$E7C2F97B-99F3-4A98-B5F0-E15506245012","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"44b9bc61b17adec77fbe5c9b86c10a811a930765","datavalue":{"value":"W2810373436","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1656596$23DF14F8-E978-4F0F-8C8D-6D784207231F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"792c0ae4f0f9f08dfa7e1830872f85395afd8e03","datavalue":{"value":{"entity-type":"item","numeric-id":2410575,"id":"Q2410575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8912f0f9f82585b06ae4de68ae0140adda1934f2","datavalue":{"value":{"amount":"+0.7114911079406738","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":"Q1656596$984EAADA-9D81-4EAF-BDC8-819C733237AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2bef11032a86e0846a0cc529c96dd87c17b04901","datavalue":{"value":{"entity-type":"item","numeric-id":3636883,"id":"Q3636883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4691c2a355ca749305e2ac84186f9b413ddbc850","datavalue":{"value":{"amount":"+0.7027865052223206","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":"Q1656596$5ACFEFF4-55B3-42B7-B5E6-61D8454165EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a522abc1d0facdf5ef53f3e0d69cb49580d40703","datavalue":{"value":{"entity-type":"item","numeric-id":2287069,"id":"Q2287069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d820bae600348acfe16dcd5d2eacef7ed19288e1","datavalue":{"value":{"amount":"+0.6991931796073914","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":"Q1656596$64678C3E-ECA6-4EA0-9112-E0C773A6BE6A","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":"444ccb72190f4e3a9cabe9953b731c867555fe69","datavalue":{"value":{"amount":"+0.6953548789024353","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":"Q1656596$A01BD1DD-59D8-4874-8F36-39C6F1D26476","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f135000cfb5801f33f862789e630b25bcf69549","datavalue":{"value":{"entity-type":"item","numeric-id":6160910,"id":"Q6160910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f658d18cee03d1f83c9d9c6290f3e416248bed75","datavalue":{"value":{"amount":"+0.6897954344749451","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":"Q1656596$A1080361-C0FE-406A-83F8-188BFEAD2453","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Effective_use_of_SMT_solvers_for_program_equivalence_checking_through_invariant-sketching_and_query-decomposition"}}}}}