{"entities":{"Q3081445":{"pageid":3092160,"ns":120,"title":"Item:Q3081445","lastrevid":58105890,"modified":"2026-04-03T20:07:05Z","type":"item","id":"Q3081445","labels":{"en":{"language":"en","value":"Backward reachability of array-based systems by SMT solving: termination and invariant synthesis"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5862393"}},"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":"Q3081445$1D65618E-4A48-4839-B59D-70E7B56C7130","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dd9b52bd2539ab7f96cf04b1c53f83564557c808","datavalue":{"value":{"text":"Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3081445$798DD7AE-7858-4DE9-B275-DEBE8E8B74AC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2ca4d4bce57d4fc2741208739278a57fdfc44c4e","datavalue":{"value":"1213.68379","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3081445$6D7A7F12-6428-4AB9-9486-8D6869EBD56E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"73649ca8b11f82b5c66947ad2623f2d7f6febbd4","datavalue":{"value":"10.2168/LMCS-6(4:10)2010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3081445$B27D62D6-3E0B-4D57-B91C-A84AE10217DD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"44f075398e4ccd740a9ac00697271020232935ff","datavalue":{"value":{"entity-type":"item","numeric-id":284229,"id":"Q284229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3081445$4AAC6C4C-353B-46DE-9A3C-2B58DDDFB404","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7a648f5f5c43d7007feb24ddb34b99c77877b620","datavalue":{"value":{"entity-type":"item","numeric-id":219438,"id":"Q219438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3081445$F132BB85-2036-40D0-BB7F-AA39506F5EEA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3081445$105990A4-1832-4DAA-888C-BBD50055AA76","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4a7583b1e3be50fc6ea49700c35e083b5398d19a","datavalue":{"value":{"time":"+2011-03-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3081445$7BA72B2C-9D88-412E-9A6D-2AFE7ECFE1BC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"52381717e66918ac18ab76d710435407ff31826f","datavalue":{"value":"https://arxiv.org/abs/1010.1872","type":"string"},"datatype":"url"},"type":"statement","id":"Q3081445$3F5AEB3B-9FEF-4AB2-B3AF-8118D58C8A5C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3081445$AD43A2BA-1AFD-453C-8DB6-69F0A35BEA7F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9e8f822d76e563407c8057bcbfb2e79873fbc25c","datavalue":{"value":"5862393","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3081445$D6EE1747-1358-4DD5-9EB3-88938F88FF51","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"585dc6257f5929a99f6f429d150f2cb62788f36a","datavalue":{"value":"infinite-state model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q3081445$71F36338-DA9B-44A5-8749-613A25D7335A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q3081445$6EC65F57-48E8-4C23-AF52-AA0542545167","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9338a342dca838223bbddb466cb122816e01ebf7","datavalue":{"value":"backward reachability","type":"string"},"datatype":"string"},"type":"statement","id":"Q3081445$7C42BCEB-6C3E-4CBE-A1A1-6BAC8784631B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"535f65541f41a57140701ba196c6989224dff34b","datavalue":{"value":"invariant synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q3081445$558A1EE8-EEC6-41C4-9CE3-7BA9DD9F8596","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"28878982f6f1ce573a5e23c591a450c4338886eb","datavalue":{"value":"safety problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q3081445$3E211951-1539-4C9D-AC9A-18791C5F2612","rank":"normal"}],"P1463":[{"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":"Q3081445$4AA8C850-4C29-4E02-B87A-1D25DCADC6B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2c19906f7a381f985883f63cec5e8a507a13287f","datavalue":{"value":{"entity-type":"item","numeric-id":16310,"id":"Q16310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3081445$3570A029-1DD0-49AC-97E8-FEF6C354B11C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f72920035b67b72d36194fa1cacb9706003d48fb","datavalue":{"value":{"entity-type":"item","numeric-id":23847,"id":"Q23847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3081445$69652226-6DB8-4CE4-9C54-DBB949C797D1","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":"Q3081445$E5AD875B-578B-4591-99B4-77A027792D06","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2aebc0f97f3943a6be87ad58d10111a7b2f37982","datavalue":{"value":"W3104749005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3081445$C0A1B821-EA56-4435-B958-49351083D897","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7441d0ac138a42ca07544f96589c657fae15c5d5","datavalue":{"value":{"entity-type":"item","numeric-id":5178977,"id":"Q5178977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b03b1bf3e829f2ed8a481e20c3b29bdae28ac75","datavalue":{"value":{"amount":"+0.814541220664978","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":"Q3081445$1593A85D-5F39-439D-BA2C-3AB938EC2E9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5374a685b3ad64a9cc08b51af3ff70626b89f79","datavalue":{"value":{"entity-type":"item","numeric-id":5747748,"id":"Q5747748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e18feab524404216ae8bb8fe4257deb480e4120","datavalue":{"value":{"amount":"+0.8077532649040222","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":"Q3081445$CE8C6608-D607-45A7-AE23-0C786778C281","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e06016963fa7603b778e3bb1f46482d10e1b53c1","datavalue":{"value":{"entity-type":"item","numeric-id":3648730,"id":"Q3648730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b7b4ac0bbc74284ef03889739e1d7700f4a9dc83","datavalue":{"value":{"amount":"+0.8059809803962708","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":"Q3081445$99DA9E7E-5949-4C03-B531-439DA7B3164B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bddafda16883dbf41636293813aa648ee5334931","datavalue":{"value":{"entity-type":"item","numeric-id":2841996,"id":"Q2841996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"23df1ec5691425a6a8e121d512e697c763ba7889","datavalue":{"value":{"amount":"+0.7989282011985779","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":"Q3081445$B7A58D4F-E406-47C4-BD21-668078BD3A98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbe651991cbc4916826a09c50dbc4cb815d3f966","datavalue":{"value":{"entity-type":"item","numeric-id":3541687,"id":"Q3541687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5aae641035badb8651d87e4c59dea00f79d658f1","datavalue":{"value":{"amount":"+0.7921621799468994","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":"Q3081445$1D8F659D-4BBB-431A-A95F-C687C93B2CB1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3081445","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3081445"}}}}}