{"entities":{"Q1703012":{"pageid":1713753,"ns":120,"title":"Item:Q1703012","lastrevid":72819663,"modified":"2026-04-14T08:03:27Z","type":"item","id":"Q1703012","labels":{"en":{"language":"en","value":"A unifying view on SMT-based software verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6845817"}},"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":"Q1703012$04F190B3-5C42-4269-A8C6-9D8856386AB0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4b77ab549315425195630740106f64902a9de00e","datavalue":{"value":{"text":"A unifying view on SMT-based software verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1703012$A8E054AC-7643-4B0B-A955-F233C7317E14","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bcd76417420efc3f0b75f22ee43a8e45facd0657","datavalue":{"value":"1426.68041","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1703012$5BB1CB47-5752-498C-AC41-F9C59B1FAAC0","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":"Q1703012$BE13512E-8681-4CC4-B1C2-CE2B212A8C29","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":"Q1703012$25B5B42D-1A82-417B-9F1D-E89A71DF2F2C","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":"Q1703012$2123E513-F4FC-4509-A7B3-737049A4FCB1","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":"Q1703012$741FF116-5C3F-4F3E-8425-F9C60EB3A948","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3ead1def560b38beae02ca12f5c5bf33059d8b8e","datavalue":{"value":{"time":"+2018-03-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":"Q1703012$F6951410-26AF-4CCF-80FA-D3698CD393EF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1703012$3EFDA398-CBE1-47EC-A43D-BC2B3AD922C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1703012$F7243F1E-49A6-4CFD-9579-5F313BE4AF2E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"62124e325ccf591ef8bda8b598e8366f18420fd7","datavalue":{"value":"6845817","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1703012$52A6FA4E-8094-452B-9F04-B8728F9228B0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff93fcab863d9a2d7b61f398ca8507531735efa","datavalue":{"value":"software verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1703012$DD728F62-85A5-4B74-8A75-3389230185C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0f668560f85d7afd1fece97b175bc3414226fbb","datavalue":{"value":"program analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1703012$F719A7CA-76FB-4D76-9ECF-E2C5C14A7B56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6ab41959fd9494b5548d09c762ca90a9336e1c7","datavalue":{"value":"bounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1703012$79D89E09-21B3-4E30-85BE-EE0357329221","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1eaeceddf514f02fd773f9b6838af990089d3011","datavalue":{"value":"\\(k\\)-induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1703012$691C46CB-0BA6-4223-B5E0-2B87CB212423","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"017c6c33c04bdabf6f732579de48e3e3f8eadfb6","datavalue":{"value":"Impact","type":"string"},"datatype":"string"},"type":"statement","id":"Q1703012$E2B9B2B1-B5D6-44D3-A49B-C1797E3CB2E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c48ac8769e1d6ddffb855348350fdf93e47001d","datavalue":{"value":"lazy abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1703012$7D089803-A77D-4354-BB63-A7FE1DDE8D55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9fb50508d9ae1a4b5b2525656ffbf4223c07463","datavalue":{"value":"predicate abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1703012$E8AD0601-1687-47AC-8367-9CEB86C0D9BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dac36a0d5bcef050bd5c5ec480998b0eb01458a6","datavalue":{"value":"SMT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1703012$A63E1B90-E9E6-4BE5-AD22-64B1C00BA655","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c4e11557fad98abdbd20c826863090d34ba5135b","datavalue":{"value":{"entity-type":"item","numeric-id":21925,"id":"Q21925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$A3F7B1B6-E1BB-4A16-A4FA-D8A89EE5ECBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f5d00c8ea90db1902290486ff0a016abf9032d22","datavalue":{"value":{"entity-type":"item","numeric-id":21461,"id":"Q21461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$B7142EE8-7A7B-4A63-B2E9-EA0AEBBA5A9C","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":"Q1703012$56465E5D-B9A7-403E-95EA-C6130B1DA1D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3fa0ba30f2225a69a75d233361703cec68c39010","datavalue":{"value":{"entity-type":"item","numeric-id":15473,"id":"Q15473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$191A3FA3-9326-4F8E-90A6-1578D436B194","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fdab07d39556d0075d882dcfd5a58c05fcf1a7e9","datavalue":{"value":{"entity-type":"item","numeric-id":21698,"id":"Q21698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$5A57A8CF-B49A-406B-AB79-6394BCE87ED7","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":"Q1703012$5E3335A4-4F65-4F93-8137-4F4F8F453A64","rank":"normal"},{"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":"Q1703012$2B7B7102-829A-4DB9-BA6B-13045C6BC8BF","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":"Q1703012$0D4793E7-3C1D-42BB-83A6-F8774000350A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a4f636583a26240d6177ac1ea0a1a2046a522c7b","datavalue":{"value":{"entity-type":"item","numeric-id":21551,"id":"Q21551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$5BDAA3A3-B749-468B-A4F5-E5CED6143DA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"550af4745ee61c125520a209383c6305679e155b","datavalue":{"value":{"entity-type":"item","numeric-id":35084,"id":"Q35084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$FD02AC21-29AD-4D8A-84D2-B0FC293358E1","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":"Q1703012$BA6A846F-D90E-43C5-B473-C01139920799","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":"Q1703012$24D75546-20F9-4C3C-977F-0B3E26565895","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d9f1915d0dd4abe9e56e462e6cb9d5d6e5b98231","datavalue":{"value":"https://doi.org/10.1007/s10817-017-9432-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q1703012$A3C8B63C-4EBA-462C-9149-900F733ABCA5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5c4457ada088b5bb1c3a7e8d68d49a1bb75e0ac8","datavalue":{"value":"W2773676607","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1703012$00A5F97B-5FC5-4C97-A626-22407E253E18","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd4a0c107773baf4c7b30e2c05565087fb2ff673","datavalue":{"value":{"entity-type":"item","numeric-id":5452362,"id":"Q5452362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$4EBAC543-0AC8-46F3-AA0D-2D44886875CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c84bacb2156f6dee41dbae90f188191d14ff028","datavalue":{"value":{"entity-type":"item","numeric-id":2894271,"id":"Q2894271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$C3430401-0C1C-4572-935C-3F120A1ADB0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83fa1aea41b23b77e49c2e6c48c1b67f2ce6b255","datavalue":{"value":{"entity-type":"item","numeric-id":4095837,"id":"Q4095837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$ED9085F0-369D-481A-B3BC-54C8D798D2D7","rank":"normal"},{"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":"Q1703012$34BAC12F-88B9-46BD-B913-C2BB6C220D36","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":"Q1703012$B28B2160-DE7D-4964-8CC3-15A56E6BB725","rank":"normal"},{"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":"Q1703012$01692234-67C2-40D8-9158-9FC838B33CD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e25f97d863b678de339f343f28e44115ff865f8b","datavalue":{"value":{"entity-type":"item","numeric-id":5452621,"id":"Q5452621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$ECEB73DF-8A9E-4F56-A7EC-F79B5179220D","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":"Q1703012$3B5F6BAD-3C76-47A8-82F3-4F53FCEB61D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"349fa0bbc46d88f17de1610f90d279b612f62ded","datavalue":{"value":{"entity-type":"item","numeric-id":3601408,"id":"Q3601408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$1A16186D-CBF7-4FE2-A370-68B915AA9880","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":"Q1703012$9B1594D6-8071-467C-A06F-E2A948C409B3","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":"Q1703012$2246DAE3-4DFA-4E5E-AAA7-E6ACF0C9890F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d0863918228d158fae088a6efc6f79f2c8e8057","datavalue":{"value":{"entity-type":"item","numeric-id":3724245,"id":"Q3724245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$77478BFA-AD93-4820-B134-B6D2C8B86178","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":"Q1703012$A6759F73-2EF4-47BF-891A-C9119F103CC5","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":"Q1703012$1EEBD1C9-0D23-4D17-B1EA-B36CE2FD31F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aee35b920b29b4f9dcb2d3243c04d909ecceb6c8","datavalue":{"value":{"entity-type":"item","numeric-id":5900703,"id":"Q5900703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$193A2EAC-79A0-41E5-989D-28D6095BDA79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"358a4e09d6cbdccb0a6a97551bee24c6efb9d080","datavalue":{"value":{"entity-type":"item","numeric-id":5326338,"id":"Q5326338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$CB786482-F5A9-4AA1-927F-D6446C937C44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c0c766394f5e5ce0b65882d3a1a29dff11575f5","datavalue":{"value":{"entity-type":"item","numeric-id":2891411,"id":"Q2891411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$1CBE4761-4987-4C4A-87FD-D1790BE295D1","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":"Q1703012$E168A162-51A4-486A-81BA-15BEE277A702","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22b34230d6df626c64dad187f872ce2d2c543952","datavalue":{"value":{"entity-type":"item","numeric-id":3081445,"id":"Q3081445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$662EADFE-E57E-4DBA-B7E1-2D9FE38BB0C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72453431b10b3f97c51f820a77b59fa085fa0127","datavalue":{"value":{"entity-type":"item","numeric-id":2827465,"id":"Q2827465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$11FCDFF7-2A04-42E0-8357-787A5C0D6C96","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":"Q1703012$CC70D5FE-C265-491A-B040-773848D6AC9C","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":"Q1703012$B4CCA253-FCFD-46C0-8DAD-88B37AE7617F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e29a9e63db651327a88d88e2cdc75e51e9cd4afb","datavalue":{"value":{"entity-type":"item","numeric-id":2843329,"id":"Q2843329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$1ED6DC8B-4051-4A0C-A0E5-A122C5F74E72","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":"Q1703012$B58DF847-FC64-439C-9B43-8F10BCE94B65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c67c1af8188e320ba0299a6df2df39f5b6e776e","datavalue":{"value":{"entity-type":"item","numeric-id":4068060,"id":"Q4068060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$5DB38F59-B7B9-4315-968F-2325F8D0DBB6","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":"Q1703012$F1461B4B-D1DE-43BE-9628-78318CF8C8F4","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":"Q1703012$2A288A15-51DA-42FB-AB1B-6BB059B014A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7ee42bcb5651ff1d6441d36735f61656172044f","datavalue":{"value":{"entity-type":"item","numeric-id":4417909,"id":"Q4417909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$BE1C70CC-1D28-4DA5-B08D-49A4937523AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5216594ab26dc420117c0934281b2e8f583a7fe4","datavalue":{"value":{"entity-type":"item","numeric-id":4255591,"id":"Q4255591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$FD63D8FC-57CD-4DDB-BDA1-B09C9F5569BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e565e03b57304d91468b39467bde71d8811efce7","datavalue":{"value":{"entity-type":"item","numeric-id":2852018,"id":"Q2852018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1703012$40122ED5-3A7C-408C-B439-7994E3AEAF10","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6a6bc212b0f93c361cd6597e601ea11c7f70958e","datavalue":{"value":"10.1007/S10817-017-9432-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1703012$78F740CD-BFDC-48AC-BBA5-258AB590D419","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49fa52d4f6f64da344488e7c632f25a795b9ee9e","datavalue":{"value":{"entity-type":"item","numeric-id":5899041,"id":"Q5899041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8b686daa569124603bffbadf155dfb7479bab9c","datavalue":{"value":{"amount":"+0.7535443902015686","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":"Q1703012$12B78925-8F63-4E1A-82F5-55289B7CDA03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c65b59f053891bc48374bd07239cf3105cdec628","datavalue":{"value":{"entity-type":"item","numeric-id":5039500,"id":"Q5039500"},"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":"Q1703012$3E22144B-3446-4D74-95E7-D10F716085F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"060b299a48c3179c59c6541e6cf5829c59574c76","datavalue":{"value":{"entity-type":"item","numeric-id":5434475,"id":"Q5434475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2307d770b0bdc8f9c623b71ffdabcc4feb6b44f4","datavalue":{"value":{"amount":"+0.7430416345596313","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":"Q1703012$3AA6A50E-F45E-4542-9CC2-F41EB341E818","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72f2beb968a92a8234db0e3ae391703a42c99f5f","datavalue":{"value":{"entity-type":"item","numeric-id":518396,"id":"Q518396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19dec90d1867c932add2a122b8330c3a00f1bc89","datavalue":{"value":{"amount":"+0.7320818901062012","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":"Q1703012$FE00AB34-1D11-4907-A24A-0E5FC9A46692","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ba55ee38a99d46604b9b2feddb9efbde5b9b1bb","datavalue":{"value":{"entity-type":"item","numeric-id":5240105,"id":"Q5240105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2a8fd5c4f2b519002a45096ecc385c71c26d23ca","datavalue":{"value":{"amount":"+0.7307503819465637","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":"Q1703012$6A88DEBD-0283-4202-8E17-99682A640D46","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":"Q1703012$52B7906B-3D26-4BE9-B07C-AEFC257A27C2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A unifying view on SMT-based software verification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_unifying_view_on_SMT-based_software_verification"}}}}}