{"entities":{"Q2958361":{"pageid":2969080,"ns":120,"title":"Item:Q2958361","lastrevid":52733309,"modified":"2026-01-23T09:29:30Z","type":"item","id":"Q2958361","labels":{"en":{"language":"en","value":"Using unified model checking to verify heaps"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6679805"}},"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":"Q2958361$D7538EBE-A2A6-4C48-A81E-696B148E4F38","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6cc7b0599751b541c85cf1d8d4cd0ba5ed39a509","datavalue":{"value":{"text":"Using Unified Model Checking to Verify Heaps","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2958361$779811A4-2EC6-4059-9512-0268EBD3A149","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7855fa307b988b37e46647a55aaac9a56195cc23","datavalue":{"value":"1483.68199","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2958361$EC2E5867-5CFF-412D-85F0-2187C3A7CAE8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"dcc31bc0a321a5286553b3dc897ea71caffa6514","datavalue":{"value":"10.1007/978-3-319-48749-6_55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2958361$369C72D2-ECA8-4ABD-9C70-D1B02CE40C43","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4bead7ac2a472d66f86a286aedbf376a64ca73b0","datavalue":{"value":{"entity-type":"item","numeric-id":1986560,"id":"Q1986560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2958361$04DFFEB1-7344-477B-808E-6C7C8FDDB5AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"30d9aa89bda10e60a2b2b6e5c4297a8a726a7ab3","datavalue":{"value":{"entity-type":"item","numeric-id":247891,"id":"Q247891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2958361$04E4B5E2-48E7-4F53-8232-A7CA898C7C11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b63c8a7d27ac589b244a048d2f920a9e8c6bd330","datavalue":{"value":{"entity-type":"item","numeric-id":247892,"id":"Q247892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2958361$7138C859-48F9-4176-AB25-AB09A8212E05","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"5ee1bdbb93e1dcf1103c5b56928114e9a720c225","datavalue":{"value":{"entity-type":"item","numeric-id":2867102,"id":"Q2867102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2958361$2C4ED501-A08A-4F03-A8DE-03578E9C984A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9849d71e29537eeb70c12e6244018ee5a71fc837","datavalue":{"value":{"time":"+2017-02-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2958361$C37AAE3B-10A5-4827-8273-EDD090CF1BAB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2958361$6233BA78-AB93-4714-9DBD-D3DA94F01E7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2958361$910CAD82-49AD-4899-83C5-FC2B4799DAC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2958361$77D58A61-03B9-46C9-B60D-BB786E23136D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2958361$2F98B3F2-3D0C-4664-86B8-5AF526791CA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2958361$6354D69C-FE62-4CFB-B1FB-C6F825A45C31","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"57849cf11c1da850da6cb62600769b4dfe8faf93","datavalue":{"value":"6679805","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2958361$1404A0D9-8E1B-4FAA-AD3B-30046E876040","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"413e452b26c4e8fa478f8075996a0c0fa61695e0","datavalue":{"value":"heap verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2958361$0C0E6B85-3EA6-4D2D-B39A-6A1D302534BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2958361$66F9D551-8463-46F6-BE9C-FA9493D10DAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"84e026c37b065e90ea6a0c462c4ada94e004527d","datavalue":{"value":"MSVL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2958361$500AAD83-97A5-4568-A5F5-4E670FC3994D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"31370a3c43d7167ff288ee84d911a7938e2319c1","datavalue":{"value":"PPTL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2958361$1E54EA0B-850B-4846-ADB4-41C76B463C84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2958361$17DE9E8B-6F9A-44CB-A9C8-4D0DA1847666","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":"Q2958361$0CA212CD-7777-4895-9458-5FB5A846B5F2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"97cc39954f9e3bf95763d3d8f3babcbe3873f8a0","datavalue":{"value":"https://doi.org/10.1007/978-3-319-48749-6_55","type":"string"},"datatype":"url"},"type":"statement","id":"Q2958361$70D3178B-B55C-4F4A-8376-D6EFB876FAA7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1066166bcf2071f4e8be6381e09882b25ccc5cce","datavalue":{"value":"W2545959453","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2958361$48ED2CF5-4322-40CB-91AE-BEAD7D0A402D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1da1cf5a701a96be6e2b4fe8962f9ab5cf74c40c","datavalue":{"value":{"entity-type":"item","numeric-id":5493374,"id":"Q5493374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2958361$8A9BA5A0-3D8F-44CA-9A5F-51162B14BCCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e17d0aa6de1a3c4e838a8fa4c7fc5c6cc0f20445","datavalue":{"value":{"entity-type":"item","numeric-id":5395670,"id":"Q5395670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2958361$29EA9003-C5E6-4033-99AA-4A800B51310B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ccf02e74786a2c5f7ea2dabcf2ee15c3dc85ab8e","datavalue":{"value":{"entity-type":"item","numeric-id":2469157,"id":"Q2469157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2958361$8B71180A-953C-4B9F-9E0E-4EC79B774D2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7050866c2121a8fe6e2a514ebee5b0e4a27e3a5f","datavalue":{"value":{"entity-type":"item","numeric-id":3424121,"id":"Q3424121"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2958361$D8095AB9-B636-4E8A-8962-920108B120F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e8499c791c9d08362181108e6d46ed350baa6bd","datavalue":{"value":{"entity-type":"item","numeric-id":3591397,"id":"Q3591397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2958361$9AF56AD5-33A6-4791-87C3-A602C69A3EB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"844ee63cb8e94ae06995eef11e72971b8dd5bbba","datavalue":{"value":{"entity-type":"item","numeric-id":835783,"id":"Q835783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2958361$3F97816B-0751-42BC-9B18-2F10EDC054D4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0ed54078757e6b23af58f39b5e54dbd5ef19d50e","datavalue":{"value":{"entity-type":"item","numeric-id":1986561,"id":"Q1986561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c071add20d9256b7240d0d6d053390c7e50ce0e2","datavalue":{"value":{"amount":"+0.9798977375030518","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":"Q2958361$F1396B60-05E9-4828-99F8-25CF6289B512","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aa7200f243c8cbbc7535d3efc4d1545d4be56548","datavalue":{"value":{"entity-type":"item","numeric-id":3424121,"id":"Q3424121"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e9b6be0c17d5bd042c58c2f47b4e10403bc4e0de","datavalue":{"value":{"amount":"+0.7800312638282776","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":"Q2958361$AB7F6552-845E-4243-91C7-8161DC073AD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"55e28678e420ac861ca2aa5c03cb223e436c57d0","datavalue":{"value":{"entity-type":"item","numeric-id":4417895,"id":"Q4417895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"52e9083b66d507dbf4e5f984115e69d544a5b9ce","datavalue":{"value":{"amount":"+0.7800309062004089","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":"Q2958361$2F0DE6F7-9A97-471F-8B97-A4F4A26BAFAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cfacba9bcb5ed4533ea46a692875a3f7c3b5f1d4","datavalue":{"value":{"entity-type":"item","numeric-id":5434501,"id":"Q5434501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b3bb30db2b93d7d30d6bda8df9ca25eaae97c8c","datavalue":{"value":{"amount":"+0.7562123537063599","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":"Q2958361$939E6084-F5B6-463F-BABF-4B74E1A2B264","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"225ec6d221f9e94e9aa6d8c24361788fd78493bc","datavalue":{"value":{"entity-type":"item","numeric-id":5394591,"id":"Q5394591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56c8c20f53591923e13a85767146722a51c27069","datavalue":{"value":{"amount":"+0.7450581192970276","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":"Q2958361$348E7CC8-50C4-403A-A467-5628B964EAC1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2958361","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2958361"}}}}}