{"entities":{"Q5178977":{"pageid":7208549,"ns":120,"title":"Item:Q5178977","lastrevid":52227182,"modified":"2026-01-21T05:05:18Z","type":"item","id":"Q5178977","labels":{"en":{"language":"en","value":"Light-weight SMT-based model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6416536"}},"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":"Q5178977$8E73F16F-D5B2-4113-B075-4E93D5E5EE54","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ea0679eefcfe31b7739f7ae4101a611f0f2fac1f","datavalue":{"value":{"text":"Light-Weight SMT-based Model Checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5178977$AF979397-8478-4068-A488-D710A4E5785E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bdca936a2eede73991089ee6bdc160ef037e708f","datavalue":{"value":"1335.68138","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178977$19B33588-5D7E-4503-9852-87FCF7B72E8C","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":"Q5178977$D7900EAB-79F4-49E4-A3D0-E01347EC0594","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":"Q5178977$547BC2CE-BFEB-4216-A8F8-DA5662F7C10D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c071f191122e8fb8fb1c63ffb2947085a44eaaf3","datavalue":{"value":{"entity-type":"item","numeric-id":5178976,"id":"Q5178976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$47CF4818-0B24-4D10-99F3-0FCE3F05E5C6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$BCC6436F-4327-4A7D-8959-D8B3418C8E79","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e3ae1d772ce191deb207c0bad17ca1d39804476a","datavalue":{"value":{"time":"+2015-03-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5178977$58870001-7EDA-490E-AB90-B17513FDF987","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178977$3BAF4589-2723-44DD-A3E5-844F735A6EF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178977$701FD74D-BC70-4054-8C38-1775AAB91E75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178977$DD9E28EF-DC7D-4247-8973-8FAB5DE3DC26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b65efe51b183d0f4a672427b8171cd1e14211cba","datavalue":{"value":"68W15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178977$1E150C27-99F0-4AE6-A760-CFE518F3825C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b10d86b354ede5a096378f6879afcefb551bc603","datavalue":{"value":"6416536","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178977$0F252049-456B-43D3-A9FF-99505731B6A0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e82e4c3b54f41ef6bc6c01269447a240723abc46","datavalue":{"value":"model checking of infinite-state systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q5178977$B6C38DF9-3898-44DF-A424-E39C8691B936","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q5178977$9B353C2A-D3D8-4CC1-A073-3CC60CC38151","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d584e359576a00f85def0b98465ac7707c1c7959","datavalue":{"value":"safety","type":"string"},"datatype":"string"},"type":"statement","id":"Q5178977$4B0204EF-4AB2-4281-AAF0-DBE342C5E6DD","rank":"normal"}],"P1463":[{"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":"Q5178977$0C70B576-0F9A-472F-98E4-394503665BAB","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":"Q5178977$D3D8E8B7-F278-4CA2-8526-CF17082A6A40","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":"Q5178977$B71A5ED0-4DC0-47E5-88CB-4873E7D4F1CD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"970eafc39a7c72dd0257d14449fe7a5c92cf6ed1","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2009.08.019","type":"string"},"datatype":"url"},"type":"statement","id":"Q5178977$98C6082C-67CC-4311-ACCE-17C7C377FBC1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"da41f9996a52ccb3f7f7478dc49b040336539951","datavalue":{"value":"W2034565311","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178977$832D7EB9-FAE5-4CE6-A210-C23A826F775A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca108e30c3fc907c7296b226db780f8d8292dce7","datavalue":{"value":{"entity-type":"item","numeric-id":5716583,"id":"Q5716583"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$FAF46C91-9834-44FB-90B3-66825F6758DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eec8f97f99a41168ef99575b9c39b6534cb2fd2c","datavalue":{"value":{"entity-type":"item","numeric-id":3967491,"id":"Q3967491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$E29BE864-89DF-487E-830D-9CF97DCEA9A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37341a061269055eb1a7c8c4e15fc80e384f1e4c","datavalue":{"value":{"entity-type":"item","numeric-id":4124660,"id":"Q4124660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$97325791-6B95-455A-995D-1AA0D0AF5334","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"55e90a14ec4dbd0be1ad04cd19a491a2868eff2a","datavalue":{"value":{"entity-type":"item","numeric-id":3051250,"id":"Q3051250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$495D8825-A7E2-4068-A118-9977276E22CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e4eab86dc21504526d3d070c41ee51a25788b51","datavalue":{"value":{"entity-type":"item","numeric-id":5429320,"id":"Q5429320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$601C85BD-BF21-46D8-8EDE-6493C4F110CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7a98dd6d97d70129a78995b432cf7ecbb251275","datavalue":{"value":{"entity-type":"item","numeric-id":5758139,"id":"Q5758139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$7BB77C56-57D3-4E0F-B949-35EC096EE5E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d6521b2af4cfbacb55e12311cb9a04d48ea2141","datavalue":{"value":{"entity-type":"item","numeric-id":5899041,"id":"Q5899041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$A80B5A6B-BF83-4CDF-A1F1-66C6D698E979","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2feb87e0fd6ab10a8f35cd44c38a5392aa00468b","datavalue":{"value":{"entity-type":"item","numeric-id":5444944,"id":"Q5444944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$63A8AB07-0EE8-4D10-A06C-7672317EDDBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$53E59205-6385-4A87-9903-3B9D078F9608","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6da6ded218db8e1aba2fc38982f0c41333c8292d","datavalue":{"value":{"entity-type":"item","numeric-id":4809077,"id":"Q4809077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$0FBDBFE7-F2BA-40D6-B904-6DBC43ED457F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82889a8aaead4f7b83d3113f27cd04ae3da7df58","datavalue":{"value":{"entity-type":"item","numeric-id":2754073,"id":"Q2754073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$73AA865F-E3D0-4A16-B0C9-E109483E741E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"555e70759b9d3f8c50939cecd8cab09c5fff9e6c","datavalue":{"value":{"entity-type":"item","numeric-id":4472236,"id":"Q4472236"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$4166A496-B768-4F81-B730-D5CD714C6D59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ca4f823ca2e82e86e612699cdb65f38c133999d","datavalue":{"value":{"entity-type":"item","numeric-id":4052071,"id":"Q4052071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$24D433E6-4611-4CB1-B284-04EABAD677B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d425524c539f34b2c20b8cfec23a758c1eb81a6","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$40670742-FAF5-4E75-9B04-8FC6E2F13D00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3c468c5df999a5df8b9ca61276e57be905929fe","datavalue":{"value":{"entity-type":"item","numeric-id":3541687,"id":"Q3541687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$587ADF83-DE59-419D-8205-F4AAE22644F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"405126dd61c0280c8a6e72613d3b0ca29345ddb2","datavalue":{"value":{"entity-type":"item","numeric-id":3126969,"id":"Q3126969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$C3E85E18-EF74-4539-BA2C-AB5E07AC0759","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04538445deb3de7cc962fa429be16220fedd47dd","datavalue":{"value":{"entity-type":"item","numeric-id":4669653,"id":"Q4669653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$E77B3395-99A8-454F-BEC8-F757E813959B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64711e2632a589e23ffd0cef677166f24eae5829","datavalue":{"value":{"entity-type":"item","numeric-id":5709375,"id":"Q5709375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$D72B7D5C-FD5B-4DB5-8656-8AC0FE8C7EC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"939285ee99fed22e57ee8f9c77da47a3f284f88a","datavalue":{"value":{"entity-type":"item","numeric-id":4806209,"id":"Q4806209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$C4D0B4C9-7793-4A99-95FA-BC62A5DC4FAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ffedd0783e404a9886f63e24289e5cccf7b96c2b","datavalue":{"value":{"entity-type":"item","numeric-id":5902412,"id":"Q5902412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$E9962780-3E5D-4457-8DE0-769DFE875900","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b1ef4c8566673a8a5c94d00ea3fc5ee04078d8e","datavalue":{"value":{"entity-type":"item","numeric-id":3506045,"id":"Q3506045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178977$554CF982-5532-4B34-A70E-D90968F8A60D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2d1a47cd62e2d8802d50ed8a6e00ef2612223df5","datavalue":{"value":"10.1016/J.ENTCS.2009.08.019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178977$8D8831C1-FCBE-42F4-B069-D632D3AD5276","rank":"normal"}],"P1643":[{"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":"f6eb82c28caa5549b99d44ee72fdebbd5a2eccb1","datavalue":{"value":{"amount":"+0.8890689015388489","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":"Q5178977$A1A2E2B0-5338-449C-8612-3029C1476D4E","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":"0418ae0cc736780b3e5adeadc197072efbee7c12","datavalue":{"value":{"amount":"+0.8226913213729858","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":"Q5178977$842C4E8D-F5A8-4FD6-B1A8-DF418BD0AA24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16f3946f85e87256de2c415f3cf1a294f0bc2ef4","datavalue":{"value":{"entity-type":"item","numeric-id":3081445,"id":"Q3081445"},"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":"Q5178977$BFA86CC6-734A-4365-B7C9-75E19DEE0862","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":"55a537a020fea6947aea67c631f3b796ee362c9f","datavalue":{"value":{"amount":"+0.767672061920166","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":"Q5178977$0C22B819-6350-40FF-874F-2D28193601A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72f2beb968a92a8234db0e3ae391703a42c99f5f","datavalue":{"value":{"entity-type":"item","numeric-id":518396,"id":"Q518396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"690c9ab1c034e3752e62bfab3d7c0b1d015cdfbd","datavalue":{"value":{"amount":"+0.7549614310264587","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":"Q5178977$B8CC3A48-D50F-4890-BF83-F842067A5920","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5178977","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5178977"}}}}}