{"entities":{"Q2409744":{"pageid":2420487,"ns":120,"title":"Item:Q2409744","lastrevid":57902484,"modified":"2026-04-03T00:42:48Z","type":"item","id":"Q2409744","labels":{"en":{"language":"en","value":"Scaling bounded model checking by transforming programs with arrays"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6791231"}},"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":"Q2409744$2375C17D-80E6-47EB-A739-70362E7B4500","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6bcb5ec5708108090bcd6282deff16ecc31e4570","datavalue":{"value":{"text":"Scaling bounded model checking by transforming programs with arrays","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2409744$7AF9ED8C-3A5A-4335-8756-C488C119DECA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"79c01a47c61d31b1da72d5f0a6147097527d99f2","datavalue":{"value":"1485.68067","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2409744$75C72A3A-A951-479B-A1F6-D2D6E1094D75","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"347d7a1cbb021c141f95595fc6ed75366f0ce9f6","datavalue":{"value":"10.1007/978-3-319-63139-4_16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2409744$88CCBEAD-BE60-4956-A1EF-FAB5D0BFC335","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"24377f25584aad3a9dc8d404c7b5a47e397178bb","datavalue":{"value":{"entity-type":"item","numeric-id":2409741,"id":"Q2409741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2409744$961B8193-B397-4FAF-B814-15CFE6E3F822","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"091a661844bdd3c719e547f78a48148dbb3498a7","datavalue":{"value":{"entity-type":"item","numeric-id":1399006,"id":"Q1399006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2409744$8B664FAD-20B5-4CBD-9513-C696085216E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"765a86c9736fe5e4113103bc490bd5d497912233","datavalue":{"value":{"entity-type":"item","numeric-id":2409742,"id":"Q2409742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2409744$775D6B44-6044-4A1C-90F3-79630B6E0D2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4426182ab210f0026cb1d2516c86321c2524dc53","datavalue":{"value":{"entity-type":"item","numeric-id":267411,"id":"Q267411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2409744$AC1E275B-095F-4760-86F2-FD016B184845","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6a786eaee719df7eda3bb57a14703c6260d8328b","datavalue":{"value":{"entity-type":"item","numeric-id":2409743,"id":"Q2409743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2409744$B1EB5DB8-F9E6-4C41-B049-D1504E232954","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bc9e63601a8e28f445aeeeaef7b99c9c03ba64fa","datavalue":{"value":{"time":"+2017-10-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2409744$3E435D8A-7159-4C9B-823B-7FBA9EC11D34","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4bb6fa6d5a17cd6371283878d5675e91fe212859","datavalue":{"value":"https://arxiv.org/abs/1606.06974","type":"string"},"datatype":"url"},"type":"statement","id":"Q2409744$7F3BC84A-7C78-4BFE-8D42-19C869B0D4C5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2409744$F009970D-EA7F-4304-BC3F-C63B232B697D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2409744$B0F9FC98-4CF1-4F89-B02F-4A4C17D6CF92","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"84febfc47c258bd85014c35347b60b2156e5cdeb","datavalue":{"value":"6791231","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2409744$641C17BB-2E8B-4A01-A322-702B4B8B0045","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"322ea768f2b97508db847d80bb51e98a654d6c56","datavalue":{"value":"program transformation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2409744$FAF24E4D-70BB-4F9B-A5E3-9DD47814886E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6ab41959fd9494b5548d09c762ca90a9336e1c7","datavalue":{"value":"bounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2409744$BD480301-CE36-4C05-BEF7-22477E1EDDC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f98b054f0f1d80c4d5f81acc12a80f93a378f42","datavalue":{"value":"array","type":"string"},"datatype":"string"},"type":"statement","id":"Q2409744$2C36330D-A32C-408B-B129-9FC34C030117","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2409744$6406C697-E165-49E3-91D5-6360CFB9ACC8","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":"Q2409744$07B7E231-1D6E-4DE0-A1A8-DDCF8FC45242","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9b7d7c31abe6cc57a0a1bc2ffd09af6342c3a2f5","datavalue":{"value":"W2963264443","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2409744$0FF91416-2BE2-4507-A782-340297D37BB3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f7bf2d7fdcea1493e50fa7a5e719edd02efd2fe","datavalue":{"value":{"entity-type":"item","numeric-id":2938066,"id":"Q2938066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54fba883d9d9137a05cba3fc7aee72203cd88887","datavalue":{"value":{"amount":"+0.89829534","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2409744$5215A56C-054E-40BE-8815-E9EFEC5776C7","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":"9fce62f54d387d38af93a753ec99eadeb7edc089","datavalue":{"value":{"amount":"+0.87955123","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2409744$C2E0586D-6F34-41DE-B297-646731441575","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"422af33120601a8100c96ced3ec5ce2187dd3770","datavalue":{"value":{"entity-type":"item","numeric-id":5709375,"id":"Q5709375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3fd4cd9a93072cb3efc0b981e134abadff853e3","datavalue":{"value":{"amount":"+0.876702","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2409744$A12ACF81-C3C6-4F82-A123-606052C54EBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b849674ba8991432d0cab7ebf1a5b8d525fc48e3","datavalue":{"value":{"entity-type":"item","numeric-id":3564041,"id":"Q3564041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6248fc5d934af1c577318047982db81def942a81","datavalue":{"value":{"amount":"+0.8765445","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2409744$6877F27C-C506-4A4C-8622-ECF6D964D5D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d0ff17ec6498d24801a74812f7e63fe7518c3c2","datavalue":{"value":{"entity-type":"item","numeric-id":2848907,"id":"Q2848907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32014f9a3fb7394eed9f85626cbc2906b6aea75f","datavalue":{"value":{"amount":"+0.873712","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2409744$F670F785-23BD-4ED3-9002-F3EBA8208C0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81d2a6c0c75db35d1a64a9e5c5907468a4789d5b","datavalue":{"value":{"entity-type":"item","numeric-id":2864381,"id":"Q2864381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d4ff210af2c3f8a84887a0614940ad7a2eb421d","datavalue":{"value":{"amount":"+0.87345505","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2409744$81FAE7C6-A30C-4C8C-880F-B5B7DF155C0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce0a6f448476e84b2b4c7d6466ed72c357cde354","datavalue":{"value":{"entity-type":"item","numeric-id":2864380,"id":"Q2864380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c18830167e1ae32d205100682e69f1fd13bf2183","datavalue":{"value":{"amount":"+0.8734116","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2409744$3280820B-C878-45D3-A4F5-660D778DF8AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43e86e4866d63f946a9dce0ff82cf98a3b2b8ce6","datavalue":{"value":{"entity-type":"item","numeric-id":5464711,"id":"Q5464711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a9b7df7cb2dc9889744dccda8f6c6dd9a21de37e","datavalue":{"value":{"amount":"+0.871407","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2409744$34924306-75F0-4FB7-A9E2-192C06330FB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d28aa0b660eb9729e912b497df1902b521e1577","datavalue":{"value":{"entity-type":"item","numeric-id":5716600,"id":"Q5716600"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c68e0d151919cdc195e6e10035ce833e63a62f3a","datavalue":{"value":{"amount":"+0.8654644","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2409744$B87E45DE-4AD3-4793-9496-8732666DAD16","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2409744","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2409744"}}}}}