{"entities":{"Q7009613":{"pageid":21560625,"ns":120,"title":"Item:Q7009613","lastrevid":81800207,"modified":"2026-05-06T19:23:09Z","type":"item","id":"Q7009613","labels":{"en":{"language":"en","value":"Interpolation and SAT-based model checking revisited: adoption to software verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8014345"}},"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":"Q7009613$317D717B-DC49-4B33-A225-A88F5D0BA7DD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f36e45455e65c422ec0722f2f17eb2266acf18ce","datavalue":{"value":{"text":"Interpolation and SAT-based model checking revisited: adoption to software verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7009613$1DD00082-0E06-468E-81AA-A777C0858F03","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0751c7145733a45ac05eba811e22cc3b4604090b","datavalue":{"value":"1560.68075","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009613$DBC028D1-D8B0-4B9A-8558-069867115048","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"da44a29e4f8f6d87a81b0fdc09ae1d4cb979ce6d","datavalue":{"value":"10.1007/S10817-024-09702-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009613$4416BC9D-C378-478E-9B51-456884B77482","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":"Q7009613$76AB04D7-E105-41F4-B033-4DDEDB33D7B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"32907325a56017b4dae5ba711bca04428c2cbb16","datavalue":{"value":{"entity-type":"item","numeric-id":4683260,"id":"Q4683260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$1245E552-DABB-4D9D-B223-0A8395016E03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1aeedce897a01f707c93fa7785addcb1487ab7e9","datavalue":{"value":{"entity-type":"item","numeric-id":1703011,"id":"Q1703011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$FD016305-5020-400A-862A-8A2855463346","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$40DFF633-8AAB-47B1-A46E-3C88595DBFDE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b6225fd2364f70e5643f17f5e8341bc2d63828c3","datavalue":{"value":{"time":"+2025-03-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7009613$97AFE329-FADF-4D6E-808A-BF4EC7643B8B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009613$F9EB5041-93C1-46A5-861F-C2C012ADB7F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009613$38C8A3FF-1FE1-432D-B450-57ACE40C2C21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009613$6351A725-D1D6-4BBC-8117-8AB52A17A3A5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"753b9f68682196a6cbcaf0ed435764f5c9248b7a","datavalue":{"value":"8014345","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009613$39637DA3-7597-448A-A9BD-6EABA8D180B3","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":"Q7009613$A52E629F-D645-412D-8B41-35FD060286F7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff93fcab863d9a2d7b61f398ca8507531735efa","datavalue":{"value":"software verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009613$F64ACD0F-423E-4250-820B-514162F33B31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0f668560f85d7afd1fece97b175bc3414226fbb","datavalue":{"value":"program analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009613$CE3672F7-F8DE-4E64-B5CE-C92118B721A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009613$009F27A3-0AE0-4EF6-9C5A-FF96FAA98119","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9bc6474ad8409ef4528af84655741b6b5be3d7c","datavalue":{"value":"interpolation","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009613$162CEEA9-7621-4CD9-88F9-D8FDB038DF64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c792faf1c8a049738036ab0ac595552cc2384956","datavalue":{"value":"interpolation-based model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009613$F24F19AE-5B83-44F4-B443-8A9F81F3CB26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e585d98415d8e91a72073008c806ee138fb65ac","datavalue":{"value":"CPAchecker","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009613$7B116537-640D-409D-BD76-8FC4421C0DE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009613$81242593-9B73-4ECE-B365-E837FCB9A59C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5867ec7b44aefc01672736513dfe6410a0300cd5","datavalue":{"value":"SAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009613$C871BCDE-A0C4-4AAD-970D-D54FC599FC89","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":"Q7009613$C0814A82-7DCA-457C-B017-0F580219CCE6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"530d4ed6d0f32858e402afd6be6ad7fdf028444e","datavalue":{"value":{"entity-type":"item","numeric-id":479820,"id":"Q479820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$E83BC1C6-2389-4E42-AB83-0009BCBB3BCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a5f7ec14119349332290c2a3236ae73e2231fc2","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$65CC69A6-F4B9-4DBD-B495-E4BAA1FBD3D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eebfbd54885f280e97728ebefc0801777abc1ae6","datavalue":{"value":{"entity-type":"item","numeric-id":5039500,"id":"Q5039500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$27219788-7828-4C6B-A952-C22E93C50267","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":"Q7009613$E2DCCDF5-F115-4A02-A22A-2C25C2667740","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bf81e90c4d39cf308573fec5a89309ffbd96471","datavalue":{"value":{"entity-type":"item","numeric-id":3176374,"id":"Q3176374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$7880D27E-1A15-4A49-91D9-41C192BB717A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad7f4489d4c89d794424e5e3872c38fe58d4c967","datavalue":{"value":{"entity-type":"item","numeric-id":5429342,"id":"Q5429342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$D9BBA017-F983-48B0-9D2D-A27EBF3FBEAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7fa47dc2bb5bb1dcf19a9463fca750d3acd35d5","datavalue":{"value":{"entity-type":"item","numeric-id":6535576,"id":"Q6535576"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$EC1809AF-4FE5-449B-A13D-F13995B90FE1","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":"Q7009613$0E0EBD9A-9DB8-4763-94D0-5A69951B3622","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6be745c1e3c92f55b154456d6a9b2f6da7bdd3c7","datavalue":{"value":{"entity-type":"item","numeric-id":3508510,"id":"Q3508510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$EFA64F7F-3344-4450-97AD-4FF7087D2FDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21640ae8e3aa02debe92970cf2184aca918b76e5","datavalue":{"value":{"entity-type":"item","numeric-id":5326318,"id":"Q5326318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$1ABCAFA9-1949-453F-AE03-7D4209E94317","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":"Q7009613$46FD64EF-E72F-430A-8843-048CDCFDD79B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60159374e2e3f1fa60e69dc94c949ae9174a77c0","datavalue":{"value":{"entity-type":"item","numeric-id":5308405,"id":"Q5308405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$05C2E985-2D05-4263-B023-96AE5ACD9654","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":"Q7009613$B463EE6C-E3DD-4243-B78A-7B9EE09FCC81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb432ba22b37fccf5faf08bce43da173c0f9c6b0","datavalue":{"value":{"entity-type":"item","numeric-id":763238,"id":"Q763238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$2E5E98B0-79FC-4FAB-8297-742EC94B2100","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf1da1b48aad7248192eb6bac6e3c0872fcb00b8","datavalue":{"value":{"entity-type":"item","numeric-id":5178906,"id":"Q5178906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$C9A797E9-FF1C-45B7-B963-E717DF536529","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c23f3beb347d9c2281547ed608aa001f62930392","datavalue":{"value":{"entity-type":"item","numeric-id":3648730,"id":"Q3648730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$DCD52F17-D105-442E-B13D-6638F9EE0328","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acde43aadb68c83ae4d51574dcef8cc0958b2d7d","datavalue":{"value":{"entity-type":"item","numeric-id":3392921,"id":"Q3392921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$F1C18146-8C9C-47CA-BCF2-41A435742863","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4e94238a6a5ddf3dd15f03313efac1f027d9611","datavalue":{"value":{"entity-type":"item","numeric-id":3452263,"id":"Q3452263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$B7D21222-987D-4586-AAF0-F48ABC5F1038","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91c21e537ab0c07b0d3849b9a7e5a291ced75540","datavalue":{"value":{"entity-type":"item","numeric-id":5178898,"id":"Q5178898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$1CE6E698-41DD-4F46-B1BE-20850EDCD9B5","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":"Q7009613$4BAB5BAD-7516-4710-9805-D9BF1FAB77B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af62bfd2162dabdadb1d68f1499174dc7482fad7","datavalue":{"value":{"entity-type":"item","numeric-id":5716597,"id":"Q5716597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$8261CD43-D5B7-4CD7-BC1A-8C8BBC0C20B5","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":"Q7009613$26CC0C3A-4A88-4AAC-AFCB-3862763C5DFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2d9d5673d377c95422809e446c2052b58cca8ec","datavalue":{"value":{"entity-type":"item","numeric-id":5756749,"id":"Q5756749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$8A0B4D1C-C2D5-4026-9D20-9DBDAD5C0CE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"09c365b9797b8b24b4bc0d80c9ea0e6e159394ae","datavalue":{"value":{"entity-type":"item","numeric-id":3176372,"id":"Q3176372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009613$6FA48064-7BF6-4D2B-80F3-F05012D01D4B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Interpolation and SAT-based model checking revisited: adoption to software verification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Interpolation_and_SAT-based_model_checking_revisited:_adoption_to_software_verification"}}}}}