{"entities":{"Q2864380":{"pageid":2875100,"ns":120,"title":"Item:Q2864380","lastrevid":79490294,"modified":"2026-05-06T14:01:54Z","type":"item","id":"Q2864380","labels":{"en":{"language":"en","value":"Bounded model checking with parametric data structures"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6236390"}},"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":"Q2864380$FE73500F-D1F4-4CAD-846A-908C977CB693","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"453270987d0e07f1678652d8239d7670a8ee60cd","datavalue":{"value":"1277.68129","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864380$5237EF21-0F9C-4842-A541-8C38068D9F91","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"03595cd73b96d5b235024b2e19a251d81caed080","datavalue":{"value":{"entity-type":"item","numeric-id":402123,"id":"Q402123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$36057B7C-6362-45E5-BE98-B209AB4C795B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d118098d92196493c0a2dbf660f2391be37ad35b","datavalue":{"value":{"entity-type":"item","numeric-id":2864379,"id":"Q2864379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$A7F12896-55BB-455D-85AA-6F94BDD8B807","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0db1c1d4758cc84ba91e5181bfa794ba378ebc68","datavalue":{"value":{"entity-type":"item","numeric-id":402124,"id":"Q402124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$07301F60-7997-4DF2-BF37-85EC1699BE84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f83abf2b01a4357b2f9d0924a417dea001e35cd1","datavalue":{"value":{"entity-type":"item","numeric-id":338622,"id":"Q338622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$7491EBD5-40E2-4FA6-864A-D58C2F38394B","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":"Q2864380$CA768FF5-00D1-46FB-96AA-3D8D9FF5146F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"deb6cb3450bd256fc635dc32234471403070c2b7","datavalue":{"value":{"time":"+2013-12-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2864380$B9CF42BB-9153-4B16-9EE5-6AD6FF15C28E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864380$4F692491-0974-41E5-9CD1-0A0FD2D443D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864380$2E24A0DF-A3E6-4F76-91A7-977D9C5B8B96","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ecb76288551e71b5490c3ef024f25f771ba44d95","datavalue":{"value":"6236390","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864380$7AC870E8-75B3-45B1-952B-746922E6CFE6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82450bed172977afbb20c270b28a2d47d2b23411","datavalue":{"value":"BMC","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864380$2FFA724D-3EF2-4132-980B-51AC5A4A3D89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cc0b00a9961434d0b0a06c75d9321cb01f9b2c6a","datavalue":{"value":"hybrid automata","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864380$0AA84483-9116-460A-BCBA-2B3B17604B9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"307ea6b29f748dabd16a3941033cb177d5c282cc","datavalue":{"value":"parametric data structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864380$A51393B4-0E8F-4F53-A33B-89145AF784ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5867ec7b44aefc01672736513dfe6410a0300cd5","datavalue":{"value":"SAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864380$4F25DDC5-36B2-4CFC-AB55-2282ED1CDA28","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$8171AEB2-B9F9-4D04-A53A-CB2B37FEE899","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b029c35ffabe60b7d29584a6d40b4cb278ba542d","datavalue":{"value":{"entity-type":"item","numeric-id":18983,"id":"Q18983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$B31DD8C5-B618-481F-A654-90D7A380AC87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$336E7F0B-31C5-49C7-A1FE-959A250D60FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cd543fd49199b1838ba332ea5e7b335fbe6c5a58","datavalue":{"value":{"entity-type":"item","numeric-id":19608,"id":"Q19608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$2BE39B57-E3E0-46E3-B705-3F59A098C2A0","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":"Q2864380$78B7E18B-5659-46EF-B1D8-12E9DD3F0A30","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"35085cdb4c99dea83cdc306d0e0b11710080be1e","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2006.12.019","type":"string"},"datatype":"url"},"type":"statement","id":"Q2864380$673382BB-0C10-4BCA-8CFF-319B1B3BFD26","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"79aba973d441e84474c7c895c00714e8324b2d40","datavalue":{"value":"W2113236984","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864380$A76073DA-7763-4B51-A371-A0064B71A255","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4f341c6f254e4778fd7612981663d8b8703db9","datavalue":{"value":{"entity-type":"item","numeric-id":673868,"id":"Q673868"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$33C98EF8-78E1-40F8-B18F-9CB4F372967C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f71dd5571a3c1c99537e11b357ad1449f45692c1","datavalue":{"value":{"entity-type":"item","numeric-id":4809056,"id":"Q4809056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$8CA66982-7EFE-46E8-90B7-09F0A63DF48D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93883db00833e89e855c8e92c4e962692b3eeca8","datavalue":{"value":{"entity-type":"item","numeric-id":4422082,"id":"Q4422082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$5E6DA6AC-08CD-45B1-B6FD-E72E32671DA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9be67f799ffc5b3fd133657f657d0609a463820d","datavalue":{"value":{"entity-type":"item","numeric-id":5312942,"id":"Q5312942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$22ACBEA0-BC71-4139-9739-B3485018F0F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5e59694ba693ed2b8af4b0c9c848f2b45a00bcf","datavalue":{"value":{"entity-type":"item","numeric-id":4817533,"id":"Q4817533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$3D26BE2A-A56A-49AA-BC86-05AA3FB372DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a179078c9a9f8b24e5164f170dbd1be09ede2650","datavalue":{"value":{"entity-type":"item","numeric-id":4551177,"id":"Q4551177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$B25B9BC5-5071-4FA4-AFCD-94C58931D6A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$B9387C6D-6992-40D7-ADD9-C8499DF5DA6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$2E112B14-AE22-443E-A415-859512D43840","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e126d7bd7c2e5801d6bab93c4bc91a314be0dab","datavalue":{"value":{"entity-type":"item","numeric-id":5312896,"id":"Q5312896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$15403AE7-076A-4D1F-8FDF-097C2CFA2E9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"437329fbe1874c3df0014b9270301ec7c179dd5d","datavalue":{"value":{"entity-type":"item","numeric-id":5900667,"id":"Q5900667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$0835B922-EEC1-45AA-903B-6D24C27CE5C4","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":"Q2864380$B0F92099-818C-453A-8C63-74FCB4DF7E83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0870e13c4a5dd2b1ec6ccf0eb8fddafbaa000d2","datavalue":{"value":{"entity-type":"item","numeric-id":5713732,"id":"Q5713732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$0CD6FCDC-202B-4D26-875E-AC20C5C80472","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e1218a29a5c78aac47d3b3acd08ffa2daae7e8c","datavalue":{"value":{"entity-type":"item","numeric-id":5897077,"id":"Q5897077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$BD04358E-A177-46A3-8A41-0FD4DC5DB7F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3348c4f23a620a7654545e9e3737b9f755ba6069","datavalue":{"value":{"entity-type":"item","numeric-id":2643301,"id":"Q2643301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$AD82981C-A9D1-4EB5-A174-759FAEDE603C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"043b92649e7ff029c15ec8b6960da0e04c1ae254","datavalue":{"value":{"entity-type":"item","numeric-id":4503930,"id":"Q4503930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$6FD9BFAB-EEC2-4E68-B3B5-3CB9F59C2204","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":"Q2864380$209284C6-A23C-4393-A066-A29C6D5945FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9269e64d2adca53bb2f298ca1a02b550d98c27a7","datavalue":{"value":{"entity-type":"item","numeric-id":4571400,"id":"Q4571400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$0183C456-3786-4F2E-B169-12793F6F9F2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53e31460d03447356beb6dcb816454c7cb3b6e4f","datavalue":{"value":{"entity-type":"item","numeric-id":5392293,"id":"Q5392293"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$845C6EE1-5029-4262-8F74-690EC38F9C4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6122a690b53da78bbd661f67fb142d629fd3a5f8","datavalue":{"value":{"entity-type":"item","numeric-id":4787213,"id":"Q4787213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$3ADD9F05-AFA7-4BB4-9364-B7F2FE63092A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2fcc34fa306d394c8abcc877cfde68c3a20ea339","datavalue":{"value":{"entity-type":"item","numeric-id":1878909,"id":"Q1878909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$C5269C8A-E18C-48D6-9C76-D43605167492","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e98bea2faf0f1e7139247049b725eb54de257627","datavalue":{"value":{"entity-type":"item","numeric-id":5593816,"id":"Q5593816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$08572412-2246-4AAB-90C7-753B4414680C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"55a413c2cc01c991b0951c4f612aeed21da026f9","datavalue":{"value":{"entity-type":"item","numeric-id":4461759,"id":"Q4461759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864380$C651A1C6-E23E-4374-8435-30C30713DF3E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0e9771603366005f00e7f79d3658addb4a3ba1c9","datavalue":{"value":"10.1016/J.ENTCS.2006.12.019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864380$0F082018-0F95-4621-9323-36FCA3532571","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"93528bddeebd8ca136ffe5b72199daed38c56afb","datavalue":{"value":{"text":"Bounded model checking with parametric data structures","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2864380$E43B13B7-C37C-4DD3-9733-D5A111C60E9A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e60d6908af4133947bcc00cf07ca518f9f650bfb","datavalue":{"value":{"entity-type":"item","numeric-id":5711504,"id":"Q5711504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1cd1149aaad0355fdab3bbb565a3fafa4dda16e","datavalue":{"value":{"amount":"+0.8244360089302063","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":"Q2864380$F5292833-9976-4F99-9779-F912C81818D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a09d1b13be3e67d230b828e006bf1a305773096","datavalue":{"value":{"entity-type":"item","numeric-id":3066133,"id":"Q3066133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec17329b4530a0047b6b3112f376ae46a82eb54b","datavalue":{"value":{"amount":"+0.8062952160835266","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":"Q2864380$1345C5FF-EE82-45E3-BE3F-E594528344AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"417f3b972ebf403c2e595613f41ecaa318eb253e","datavalue":{"value":{"entity-type":"item","numeric-id":1878909,"id":"Q1878909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e124c903a529d70939507102d05633be3c16ba9","datavalue":{"value":{"amount":"+0.8058993220329285","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":"Q2864380$6A6A05C6-347C-48EC-8CFB-67ABF74AB067","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ad56d5cf5a0914eae3e1991359f1a1939c792e8","datavalue":{"value":{"entity-type":"item","numeric-id":5898914,"id":"Q5898914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd0c3e2f9480e677b2d129fab44ed4846e031378","datavalue":{"value":{"amount":"+0.804011344909668","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":"Q2864380$03019588-D0BB-4B1D-B57C-2E8199CB6011","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9c9d5fe17ec6a5506543531b83a7f2aa7be5cd7b","datavalue":{"value":{"entity-type":"item","numeric-id":2889614,"id":"Q2889614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8edba739696ad958008d6f6f2cacb181bbe5c710","datavalue":{"value":{"amount":"+0.8030829429626465","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":"Q2864380$2A490935-12EE-4400-9369-55A1924E3CE4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Bounded model checking with parametric data structures","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Bounded_model_checking_with_parametric_data_structures"}}}}}