{"entities":{"Q3620428":{"pageid":5650334,"ns":120,"title":"Item:Q3620428","lastrevid":50630570,"modified":"2026-01-14T15:15:14Z","type":"item","id":"Q3620428","labels":{"en":{"language":"en","value":"Abstraction refinement with Craig interpolation and symbolic pushdown systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5542978"}},"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":"Q3620428$B1B00194-15F9-48AB-9645-1341EFA51491","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"90e7ec1d8e8e5fc9dee05178e98c968411ed4814","datavalue":{"value":"1172.68541","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3620428$AF4EDEF5-6801-4959-8A8D-01CB3FA15F58","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5e47b8a1818346ce22bd45f99ec3c619fd43a6a3","datavalue":{"value":{"entity-type":"item","numeric-id":264200,"id":"Q264200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3620428$2D957CAD-CC9E-4FE6-BD6A-9592AF0266A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d62012c44fa6c563fe5eb1edf4cf0db84f8565b9","datavalue":{"value":{"entity-type":"item","numeric-id":396601,"id":"Q396601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3620428$DCAFD458-892A-45A0-B410-F4E40D659654","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"42938a6743e1355728dbe4fe3c3ae295737cb5ef","datavalue":{"value":{"entity-type":"item","numeric-id":314814,"id":"Q314814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3620428$FAD54A4B-E6A8-4EDE-89B1-9A86A144F2B1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a70e3fb7efc077ae8b5215707528be5246c293fd","datavalue":{"value":{"time":"+2009-04-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3620428$4EF96282-59F8-475E-A210-622E058D16E3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3620428$52823F21-D4D9-45F3-9120-F00211EEEDE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3620428$0F1FC43E-9A5A-4836-8C06-CE4B3CC9C274","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3620428$9C2F17DB-7986-47D8-AE91-38FACA428A6A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1e11c668d5aea1f34c0c6243c67f71017b15a434","datavalue":{"value":"5542978","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3620428$E1F2D0EA-E45E-4E33-8DF6-CD1D0F911D3D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"379a567f0f983e236f95705804d342510fc41004","datavalue":{"value":"model-checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q3620428$D6B6EF15-13D7-4471-948A-B7F91C17EEA3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6e027bf88ee7cfe985b42e564a22fa6632f8a570","datavalue":{"value":{"entity-type":"item","numeric-id":14221,"id":"Q14221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3620428$F6E4C229-90CB-43CC-9118-4D45645A4768","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5d833769bb052473ef506c39280edaf1ab0ee4b5","datavalue":{"value":{"entity-type":"item","numeric-id":14928,"id":"Q14928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3620428$E64B28E6-B1A0-4C71-83DC-635FD62429C3","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":"Q3620428$F16A6803-A3AC-408F-90F1-FB44BBC504C9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d7b7a8c6f01dfecc18f5236dd4a0db19a4b41985","datavalue":{"value":{"entity-type":"item","numeric-id":5899075,"id":"Q5899075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa31bb63defa7bd8dc1f8a803d81bf10d6667a76","datavalue":{"value":{"amount":"+0.9759255647659302","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":"Q3620428$F6F24E77-A69A-423B-B9CD-C46B7DF3D8B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"848e3b605810f96456fa950cb0b05cab724cc2a3","datavalue":{"value":{"entity-type":"item","numeric-id":300418,"id":"Q300418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a6ee0e3aa1cc3914bc3c5efe704321280d81884","datavalue":{"value":{"amount":"+0.8410190939903259","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":"Q3620428$24C5F1D0-2DFB-4803-8DAB-183B3682EB1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cdd4cf7bbbfb99f3d4855a1a4e443e817c997ae8","datavalue":{"value":{"entity-type":"item","numeric-id":3452263,"id":"Q3452263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5987a20219ae3508ed76219f6b786206b558e744","datavalue":{"value":{"amount":"+0.8329841494560242","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":"Q3620428$AE349F4A-85E7-40D2-A5C7-A3DE86733785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"35471693b9b81aca4d54d85b5e7a7d84e4829dbd","datavalue":{"value":{"entity-type":"item","numeric-id":5756749,"id":"Q5756749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16b9cf30fb709cf8c0541c480eb5d7ee2563c95e","datavalue":{"value":{"amount":"+0.8160675764083862","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":"Q3620428$9E009813-DE49-410C-9B1A-255FF0F36C69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"356609ae3d55d23c02586fd1f83879a316c099d0","datavalue":{"value":{"entity-type":"item","numeric-id":2754081,"id":"Q2754081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aefa03b8b2785acde100236f2b5b81777329c216","datavalue":{"value":{"amount":"+0.8105762600898743","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":"Q3620428$04DBB3EC-9F96-40D7-9C79-402EC567F353","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3620428","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3620428"}}}}}