{"entities":{"Q1650864":{"pageid":1661605,"ns":120,"title":"Item:Q1650864","lastrevid":74076807,"modified":"2026-04-14T18:16:45Z","type":"item","id":"Q1650864","labels":{"en":{"language":"en","value":"Automating regression verification of pointer programs by predicate abstraction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6903792"}},"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":"Q1650864$3BB43C73-F112-40E6-B325-44946A4B096C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2e739d02a57c4270bbef25a918ceb137f58289db","datavalue":{"value":{"text":"Automating regression verification of pointer programs by predicate abstraction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1650864$601F016B-B2CB-40FD-ACA8-4233AE324D51","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ba152009dbc4cc748a575e997de9cd7becafe311","datavalue":{"value":"1392.68146","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650864$69ACAD5A-9E98-4AD0-BA28-263CDEC096B3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1f9ef1d44371910abd48a3e315686ed4dc2807a3","datavalue":{"value":{"entity-type":"item","numeric-id":470006,"id":"Q470006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$C32AEBE8-6C71-4EB0-9438-97C4819F0DB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2c0a4237c509f19dceb169b6d7b433af280d355b","datavalue":{"value":{"entity-type":"item","numeric-id":300416,"id":"Q300416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$AEC3FC65-16C5-4DF4-83BC-DA31FDBDCF14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"54b40af6acb3456c1b6977fa01e79eec0014485a","datavalue":{"value":{"entity-type":"item","numeric-id":1630024,"id":"Q1630024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$ECCE49AE-798D-4977-AB3B-13FCAE3CBE33","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$519EED1F-17EB-4773-A61A-8589B57F7BCF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"05ab478c1b3d983a6bbb2903fa84c4982a8bb3dd","datavalue":{"value":{"time":"+2018-07-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1650864$444A4085-E28D-4BF7-9495-DF2DBF65DA0E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"78c50051601e88042b41cc51f4361648495f3c9b","datavalue":{"value":"http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-356860","type":"string"},"datatype":"url"},"type":"statement","id":"Q1650864$39203D27-E498-49F0-8E07-AAEF90C4288A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650864$F316CF49-9894-4C20-BDD5-B041B3887D90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650864$A8649E66-6B87-4E10-A645-A815EC18A307","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"50ac52fe0938ec404de86d08cc4967bc14ad6670","datavalue":{"value":"6903792","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650864$95790195-B537-4923-97C1-55BA2620894C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8018fcc8dacbcc1f18db3e2dfa50e2962efb29fe","datavalue":{"value":"regression verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1650864$8913BC21-DE33-4180-A119-B38191DDA1DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5802efce4b159c028036a07713e366f296220eb3","datavalue":{"value":"Horn constraint solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1650864$D9AF167C-AE79-4AC0-89BC-8BBAADAFFB95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4dac5de8e537c71cd90df166682399621b2f7fbf","datavalue":{"value":"program equivalence","type":"string"},"datatype":"string"},"type":"statement","id":"Q1650864$33945046-68CF-486C-BDA6-39CADCB4EC95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9e24c01f05b3a1d5399c5d4af0295e48cde1d6e5","datavalue":{"value":"relational program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1650864$380551BF-FDAF-4402-81FE-A22CA3F47DB9","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ea1fa890b2f09c8cd0bccb17957cf46696afec2a","datavalue":{"value":{"entity-type":"item","numeric-id":19731,"id":"Q19731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$27D08C40-988F-4F91-952A-A53EB041D2E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"352070f92a42ab6c0ae16e5d77d8a717bc392ccc","datavalue":{"value":{"entity-type":"item","numeric-id":19847,"id":"Q19847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$2E412129-2BBA-45F2-A02D-15D283DEF125","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$63405642-2A8B-4E3F-81CB-27C433943C0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bed14e207a3e5d28b264f36a84b777589c129ee7","datavalue":{"value":{"entity-type":"item","numeric-id":25011,"id":"Q25011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$B84B5631-451E-4F28-95C4-AD099A03094D","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":"Q1650864$604DA0E3-3289-4D6A-B018-76AA6C7B49FA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"89b679eb0937472b1bc5a918495551a0cd293a17","datavalue":{"value":"W2751641401","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650864$9B67838B-828F-4A02-ADA5-3BF718E85AE3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c89590127f5397bc8ed4b7ff89515c95d81a4f7","datavalue":{"value":{"entity-type":"item","numeric-id":3506694,"id":"Q3506694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$7FF41ECA-8060-4822-86AD-DB4ECB8AABE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13ed56ca71244e05aaac2bba4f51079d01410063","datavalue":{"value":{"entity-type":"item","numeric-id":5348916,"id":"Q5348916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$E0B252FE-7621-4C8A-BC4C-11C2B8E88C03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a003e220a607650083ae34d9089140d42d02d540","datavalue":{"value":{"entity-type":"item","numeric-id":3546287,"id":"Q3546287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$5C6B9750-C4B4-46AF-BD59-374772A48361","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"392951dc55387d91231b1fd17edb133cac1cce3b","datavalue":{"value":{"entity-type":"item","numeric-id":2914729,"id":"Q2914729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$C5DF8232-A4DB-4A2F-B929-E59573C0A85D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4242719ad3edf3bcc7dca076bb4bc02680435650","datavalue":{"value":{"entity-type":"item","numeric-id":3453646,"id":"Q3453646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$AA3C1229-0C5F-42F8-9AEE-5D62BF460102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$ED8B9810-E7F7-4B04-A248-19EB1B1ABF39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1265d63b4599a3fae507d9b15943296bbefa977b","datavalue":{"value":{"entity-type":"item","numeric-id":4066568,"id":"Q4066568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$EF94B98B-3A05-479E-9164-2FACC8B36644","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98855e5f63a687d22ad5b8fcf60eef7c9c99fe2e","datavalue":{"value":{"entity-type":"item","numeric-id":938300,"id":"Q938300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$7DADAACF-D3FE-4E2C-B391-1056CE3A3E3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cb8e50e6c3bd60a9a9a59407cf30e8e788baa4","datavalue":{"value":{"entity-type":"item","numeric-id":3618853,"id":"Q3618853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$95C25E79-3F11-49E3-AE15-A0D70CBD6624","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db584d694e65ad0d716439ab78ef423b2e14371a","datavalue":{"value":{"entity-type":"item","numeric-id":4928447,"id":"Q4928447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$F9009661-1036-47B9-A37B-366B02D86C0B","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":"Q1650864$6327BD8D-3C0D-4A51-AD13-63D9C125B5E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f5e68905953d1d1b2da4e9dccf7b3768fef8f920","datavalue":{"value":{"entity-type":"item","numeric-id":3842661,"id":"Q3842661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$2A603BE9-FE1C-4A08-9AD2-083250513501","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eaff131682deb6ad1bffecaae47bca13d452055a","datavalue":{"value":{"entity-type":"item","numeric-id":300418,"id":"Q300418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$9D223DD3-75E7-4AF6-BDC5-8B18CEB8F2A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa2ecb01d1000f707b2d4e9dd305373c58ecfc0c","datavalue":{"value":{"entity-type":"item","numeric-id":3636883,"id":"Q3636883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$AD9A683F-363C-4F01-BB08-CA57161000BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75b680461e5ca6de0dee54f39d9f7e5f4a43fc33","datavalue":{"value":{"entity-type":"item","numeric-id":2988675,"id":"Q2988675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650864$21501850-F45F-4DAF-8489-87366C764A94","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"48eb7bb45f7ecd6de9fd9ebd63f69d3083aa6773","datavalue":{"value":"10.1007/S10703-017-0293-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650864$63DF69E1-C097-4FAD-B8A7-EFFEB478EBED","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0fb92d05ad3804bd2a0edfa57fa3315eb5bd16f0","datavalue":{"value":{"entity-type":"item","numeric-id":2891406,"id":"Q2891406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32090de877b4be7947957af3bca14c7bfaf126f5","datavalue":{"value":{"amount":"+0.8028808832168579","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":"Q1650864$48C46602-D915-4399-9CBF-E1559868AF8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ee5855c264a242b41c9aca4f8fd9ebcd139f7f0","datavalue":{"value":{"entity-type":"item","numeric-id":5962972,"id":"Q5962972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7daef0e8eabb8b90827bc8551bc7088ac4899145","datavalue":{"value":{"amount":"+0.7845858931541443","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":"Q1650864$95097E9D-8EB6-4418-9E2A-5DA41273AF6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9babaf2bd52e8d0585eb0dfafb2c1d459313c380","datavalue":{"value":{"entity-type":"item","numeric-id":2908486,"id":"Q2908486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"73b7afbbee16c86f90b5c3807fd9850f60a50ea1","datavalue":{"value":{"amount":"+0.7727413177490234","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":"Q1650864$30D7FB8D-F787-4CD6-95B6-EB1621538F23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bed03ff244bd448296e984cc4bf4f360cb72a649","datavalue":{"value":{"entity-type":"item","numeric-id":4414376,"id":"Q4414376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fcd7c3ed150e05dd4a4a0d1325631a6f378e1bb9","datavalue":{"value":{"amount":"+0.755023181438446","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":"Q1650864$556240F3-AA4B-4FB0-B472-9425061A124B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea93506793d7ae3e9f100eda6c9ed8d96448d9b1","datavalue":{"value":{"entity-type":"item","numeric-id":436400,"id":"Q436400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a324e3063258dd6df512b615748bd875cbe1915c","datavalue":{"value":{"amount":"+0.75376957654953","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":"Q1650864$A9EAB052-4FC3-4BED-8D19-47D9538D0840","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automating regression verification of pointer programs by predicate abstraction","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automating_regression_verification_of_pointer_programs_by_predicate_abstraction"}}}}}