{"entities":{"Q5039500":{"pageid":7069077,"ns":120,"title":"Item:Q5039500","lastrevid":56687424,"modified":"2026-03-18T20:28:00Z","type":"item","id":"Q5039500","labels":{"en":{"language":"en","value":"Software verification with PDR: an implementation of the state of the art"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7600810"}},"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":"Q5039500$E1628997-F4D0-41B2-B88E-8DC6D6D90AF3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0fe0d47056de252c5a017ede0ad04406867d89a5","datavalue":{"value":{"text":"Software Verification with PDR: An Implementation of the State of the Art","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5039500$24479D19-3C0B-444E-9DD3-FC981922222D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e635025e1269a45c043d65a7bdf72a05df2bedb9","datavalue":{"value":"10.1007/978-3-030-45190-5_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5039500$7E6E381A-99F4-46D3-9B2C-9E48137434A0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4125ba106c69323576edaf1300fa9e74bc379cdb","datavalue":{"value":{"entity-type":"item","numeric-id":930432,"id":"Q930432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$134CC481-8CBC-43E7-8F00-925F7B7715E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"53e531027e019634c911b8920a6b3e9ca43a06ee","datavalue":{"value":{"entity-type":"item","numeric-id":1703010,"id":"Q1703010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$772AC16F-C631-41DC-A509-94450C2A5DA6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0caef843b05c7cfb5667c1a8106613cbf61a6d23","datavalue":{"value":{"entity-type":"item","numeric-id":2894263,"id":"Q2894263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$6DB5AB11-BFDE-45D2-97DD-C4F9FE76CE13","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f63eb77a6cdb61f75205564f776cc43c0ac4bb43","datavalue":{"value":{"time":"+2022-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":"Q5039500$A3C78AF1-3F2E-4341-87A8-77C32055582A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e47e89279881b92cbe5c760d3a84ba220a203bd6","datavalue":{"value":"https://arxiv.org/abs/1908.06271","type":"string"},"datatype":"url"},"type":"statement","id":"Q5039500$43A06DF1-BABE-484A-AB9F-768754291DDC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5039500$C9542B60-721A-4F6E-86EC-6637BEBEAB9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5039500$66F91FFE-E3AC-4D01-B228-61242EA6EE70","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ae93e584daa0822e689a68f55ad10b37a7592279","datavalue":{"value":"7600810","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5039500$506B8BE1-554C-49EA-B766-F610182CC422","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff93fcab863d9a2d7b61f398ca8507531735efa","datavalue":{"value":"software verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5039500$0106FDE9-18C7-4D17-876D-4201B1EAE054","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0f668560f85d7afd1fece97b175bc3414226fbb","datavalue":{"value":"program analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q5039500$FE3AD31C-67B4-4559-94CD-F5F99E7B4D97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e4824208d7bba949dd72987d32ffb13493eeb0e","datavalue":{"value":"invariant generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5039500$D3DCB302-8ECD-4BD8-96BB-32A1AF687559","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"15e82007957ca51d35e3c74f5c2edf8ad921d336","datavalue":{"value":"property-directed reachability (PDR)","type":"string"},"datatype":"string"},"type":"statement","id":"Q5039500$A90606A9-DDED-436D-BAB3-B50EBC2E66B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a122d9ad0bbbbdbf6445cb067f20e2a2142919cf","datavalue":{"value":"IC3","type":"string"},"datatype":"string"},"type":"statement","id":"Q5039500$CE4B633A-5689-4447-8372-6F1C93D431C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1eaeceddf514f02fd773f9b6838af990089d3011","datavalue":{"value":"\\(k\\)-induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5039500$2903A3F5-A361-4092-B598-25AAE5717E48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"637f4bdb8ba5aca93ec36936c947b16c61d2582e","datavalue":{"value":"VVT","type":"string"},"datatype":"string"},"type":"statement","id":"Q5039500$8E9A90EF-3C01-4A2B-BDCF-C176A519D5F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e585d98415d8e91a72073008c806ee138fb65ac","datavalue":{"value":"CPAchecker","type":"string"},"datatype":"string"},"type":"statement","id":"Q5039500$0F3E79F1-FFE2-4F51-827A-976C57D09393","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"18407fbdc0151f0b5ba9a01c199138cbfc2a4f45","datavalue":{"value":{"entity-type":"item","numeric-id":35083,"id":"Q35083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$89586803-5123-4CDF-8006-63C84CFB95FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e1655b290b91a673f0538ce14f6694f64d961977","datavalue":{"value":{"entity-type":"item","numeric-id":19440,"id":"Q19440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$E61F8522-0459-46BE-9BDF-1515D6D8B131","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3100986a2f21986377b1ad1ea1633be0427ca603","datavalue":{"value":{"entity-type":"item","numeric-id":32990,"id":"Q32990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$AF125732-6DBF-447B-8D8C-9277DB4FE8F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0c2e88c3e093f252840def020d846265cb56777f","datavalue":{"value":{"entity-type":"item","numeric-id":32840,"id":"Q32840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$060ECDA6-AC66-4A62-B0B2-9AF15E70A840","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"69f362165978cbf04e5b5460992bc38f4ae05985","datavalue":{"value":{"entity-type":"item","numeric-id":30117,"id":"Q30117"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$F7A4404A-0552-4D26-A2DE-D424E8C8C8C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a1d6b9e920f2e41a66a9767e31ca972ed7628dde","datavalue":{"value":{"entity-type":"item","numeric-id":15668,"id":"Q15668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$868F333D-24E7-4D55-874A-85A62A040FC0","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":"Q5039500$4CFE80C5-17D4-44EF-AF66-F0276EEF84A5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"033ccf1c4e7fa83c3004f4486a9d43040e4d84d2","datavalue":{"value":"W3016403159","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5039500$929F589F-9361-4C24-B91A-E197D2E45079","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbd5e9b7224b44a5be727c6870f16a737b8c3625","datavalue":{"value":{"entity-type":"item","numeric-id":2769592,"id":"Q2769592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$1ED23058-8BB4-4C15-972A-C427C35DEE60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc25af5045c856aadb22057606de79dc70eaee2","datavalue":{"value":{"entity-type":"item","numeric-id":1703012,"id":"Q1703012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$EB88237C-82D8-4B7F-81DD-FBE51860A1CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef9a85754f10c794d7ea794155cce4bd2f066956","datavalue":{"value":{"entity-type":"item","numeric-id":3075471,"id":"Q3075471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$6D4567D3-4681-49E0-8FD8-1E55033B879A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bcdd88c0187437df1dd77abdaba504f2664c711b","datavalue":{"value":{"entity-type":"item","numeric-id":939166,"id":"Q939166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$6EC7E5A2-FCB4-4239-B10D-1BAFC9C1BD9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a721eea058e807770cf825065bd252a7ab7056d","datavalue":{"value":{"entity-type":"item","numeric-id":2363814,"id":"Q2363814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$F3CBCA6A-41D7-4F64-A990-4B461AE51529","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b026130fb14abb6ec25af9a49779c945ecc8f0fd","datavalue":{"value":{"entity-type":"item","numeric-id":3452508,"id":"Q3452508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$AD3C8F34-FE81-4264-A9C3-87661782A4F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8971435217b64c50e375aec68a6c58475d8d0dd9","datavalue":{"value":{"entity-type":"item","numeric-id":3249759,"id":"Q3249759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$944A8F1C-2250-4A46-9D09-1AEA29AB10D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4a42b76ec81d1d9fb0c3efe48d104aa5842d376","datavalue":{"value":{"entity-type":"item","numeric-id":4930734,"id":"Q4930734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$2BEE8C01-5708-4FA9-B487-F8CDDBF32F64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0be6c53659cb8642df272cd13aa4516eec9a3f8","datavalue":{"value":{"entity-type":"item","numeric-id":5228112,"id":"Q5228112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$4653F6DB-B151-4D74-8C62-1CBD620FAEA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2de737d9a4fce3456475ca3f6211de470215f1cb","datavalue":{"value":{"entity-type":"item","numeric-id":5883575,"id":"Q5883575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$5BF8E102-CB4E-4D9E-8D5D-43EF6BDD6695","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"348369ca3fccbe91226809a75cbf31afd7f3186d","datavalue":{"value":{"entity-type":"item","numeric-id":5900666,"id":"Q5900666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$94C23065-CD1F-40CF-878E-8AC2DFE77322","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a601b7873b1373e7aa846c82044f5ed1d504783","datavalue":{"value":{"entity-type":"item","numeric-id":2796039,"id":"Q2796039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"033dae0640800c533f73acf09c44e884c27085f2","datavalue":{"value":{"amount":"+0.7909162044525146","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":"Q5039500$F643540A-1CF0-404C-B578-47C6359F0443","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72eee10c46f0242c8b24ac5a879173bbcde6f88b","datavalue":{"value":{"entity-type":"item","numeric-id":4979439,"id":"Q4979439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fbb2064c92b636cc7b775bd8c571670bccf0d7a4","datavalue":{"value":{"amount":"+0.7503434419631958","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":"Q5039500$D5924CB8-699A-447F-BE9E-D3B0C78BB385","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e7efe3f01bdfd05a10577c3e89926fa8a48ca69d","datavalue":{"value":{"entity-type":"item","numeric-id":1703012,"id":"Q1703012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c935a4d1e6b412ff8b9a1db1709b5f1d7722fd2d","datavalue":{"value":{"amount":"+0.7499935626983643","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":"Q5039500$E9D552CA-741E-4BFB-8F31-E1671930673C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"309d47001d388616676746d4877f00d336c2fb12","datavalue":{"value":{"entity-type":"item","numeric-id":947794,"id":"Q947794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"55837ca4e4732ca95842641f8c20e253a30f34e6","datavalue":{"value":{"amount":"+0.7388515472412109","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":"Q5039500$4DBD3BED-9FDA-4B4B-B8E3-36029E8F1A82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf6ff91e010703ee4fbad84024e8d0fa028fb1cd","datavalue":{"value":{"entity-type":"item","numeric-id":2843329,"id":"Q2843329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40d69713dfcd8138e71496610431e4e2249f0801","datavalue":{"value":{"amount":"+0.7346423268318176","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":"Q5039500$B38B02D1-4038-4B6F-8450-E20EA4358D35","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5039500$AB5E9971-936D-47F2-B2F1-4C61798F1844","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5039500","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5039500"}}}}}