{"entities":{"Q2145317":{"pageid":2156060,"ns":120,"title":"Item:Q2145317","lastrevid":54342938,"modified":"2026-01-26T16:23:42Z","type":"item","id":"Q2145317","labels":{"en":{"language":"en","value":"Backward symbolic execution with loop folding"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7543908"}},"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":"Q2145317$B905F890-663A-4D5C-9D02-5C3200AB4E58","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a5546c37a680d0f370fa0a663d0f5760ccc87501","datavalue":{"value":{"text":"Backward symbolic execution with loop folding","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2145317$8916D0EB-6B94-4EB9-90E9-B98BC9DFC52B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e11fec3241138c1d65194bf43b08997078d40d1c","datavalue":{"value":"1497.68109","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2145317$1750BD25-21E0-4298-ACB2-DD2252C45F05","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d82808bd71b0b633289b314c46e7308a7ee2fc77","datavalue":{"value":"10.1007/978-3-030-88806-0_3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2145317$DE672DE3-8295-45C3-AAFA-4A95B3586F71","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"475c4ef013e5c89c5643b32e84e4b5c263bd3d4b","datavalue":{"value":{"entity-type":"item","numeric-id":832314,"id":"Q832314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$B98EC7FC-B709-4196-A9F2-62B9AB63D18F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"952e13cf13a37e2b25a37008848ccc82d63b7b29","datavalue":{"value":{"entity-type":"item","numeric-id":832316,"id":"Q832316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$D7F29AF3-C677-46E8-966F-08E5D1983A1B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eb05ecdd4c1bc9bc017712b48f5ce5d7c83890d5","datavalue":{"value":{"time":"+2022-06-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2145317$6877B7A7-22B3-4D7A-B273-99D15D1A95B9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2145317$23A8ED6E-34A8-4841-970B-14662BB7139B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"78fa8d1a25bb0f412913db048cc9428dcfee48bd","datavalue":{"value":"7543908","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2145317$E151559A-EACA-448E-B0D5-C2BB06B8DAAB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c35a4242d5a7b403b26733830f7ae50eea62072a","datavalue":{"value":{"entity-type":"item","numeric-id":15473,"id":"Q15473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$F30CBEC0-A97C-4CB1-B477-378AD4D6329F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b345502c513dc247f853426190dd82b49384e626","datavalue":{"value":{"entity-type":"item","numeric-id":5458338,"id":"Q5458338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$15B63E1B-D1DE-4039-9CE9-DC7F4018AE4C","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":"Q2145317$92F03E16-54D6-4DAB-8FE7-87E96FB37B09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8648065c5304ef1ccb162c9107cef4a4c44591f7","datavalue":{"value":{"entity-type":"item","numeric-id":1391929,"id":"Q1391929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$9EA56469-C9FE-48E2-AACB-0DE9049B3CA7","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":"Q2145317$449D8619-E5A5-48EF-95BF-5D7C749D4717","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67b8a6374b4fc895d89506f759c76e54380f8254","datavalue":{"value":{"entity-type":"item","numeric-id":4144755,"id":"Q4144755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$BB0CE06E-1747-4884-849B-6CF8D71A9A83","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":"Q2145317$5C0B22CC-21CD-4710-B93A-68FC7D531FF3","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":"Q2145317$97C78979-DA40-48B0-9BBB-429E988E4F2E","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":"Q2145317$CEB58911-9AC9-43AA-9DE3-A6688FC56F10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa4f96e3374f503888e2094fc6f99dfeaa211ed5","datavalue":{"value":{"entity-type":"item","numeric-id":5039502,"id":"Q5039502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$4383C997-06A5-46DF-A230-36F13BEC564B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec836a3fc271e588c302d19e3fc45042d720ac9c","datavalue":{"value":{"entity-type":"item","numeric-id":5255061,"id":"Q5255061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$A82D16C0-B8EA-4A0E-8E71-F247A9134C0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5deaf0cccbcd91007881f1158a0f8b6702383fda","datavalue":{"value":{"entity-type":"item","numeric-id":3612009,"id":"Q3612009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$D973E3B9-279D-4CF7-A7D6-785FE74F2369","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"761a583f69cec4c5be8f04f0c50f6850fd320730","datavalue":{"value":{"entity-type":"item","numeric-id":5255063,"id":"Q5255063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$3B14E056-1748-4B8B-8A42-FAB2A67327D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b93484e8ec220b261cb764722c283ac67e15d023","datavalue":{"value":{"entity-type":"item","numeric-id":4060384,"id":"Q4060384"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$9F3C4377-A1B8-48AD-89FD-314F3F248FAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"63d6099524e3f7bed0ce635b8cc10b44d3701853","datavalue":{"value":{"entity-type":"item","numeric-id":4649296,"id":"Q4649296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$9250ECFF-5C1E-4ED4-BDC0-92EA6E311223","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"efbb1fc9049136188bed4e2121aca516a730c09c","datavalue":{"value":{"entity-type":"item","numeric-id":5408447,"id":"Q5408447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$9E150F8D-3548-488F-A31D-AC0248FAD3C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"32cf75770c4378a7060a1800d601a78571430882","datavalue":{"value":{"entity-type":"item","numeric-id":3176373,"id":"Q3176373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$99E5B886-67FF-4C9A-A3D0-C3C19FB1EE93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4feebad8575c91f403302f1fcff58cdee3e55290","datavalue":{"value":{"entity-type":"item","numeric-id":1238409,"id":"Q1238409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$DDB11DB5-910A-4E01-945E-4FB517351A0A","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":"Q2145317$B99F44AA-2514-46ED-808D-B14A38AF87FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce5a4d6dd5f0e7356ed8d1127addf4b8632b1c04","datavalue":{"value":{"entity-type":"item","numeric-id":6194955,"id":"Q6194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$5E91D65D-20B5-45FA-A4BE-9F5A405DAE28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cff75baea05c748f9ad363c0a0f9a8b26cebdcc9","datavalue":{"value":{"entity-type":"item","numeric-id":835051,"id":"Q835051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$139E8BAF-FD2C-4F8C-9999-FF178092BCF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"437329fbe1874c3df0014b9270301ec7c179dd5d","datavalue":{"value":{"entity-type":"item","numeric-id":5900667,"id":"Q5900667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$B6323FFE-3BBB-4054-A98D-196DB2B11FC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ab3ce518514c1eb6a24ae802e28cbbc33a403c5","datavalue":{"value":{"entity-type":"item","numeric-id":3613374,"id":"Q3613374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$5A424C95-A37D-4FC6-8C45-7B658D8B570B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e77e4ca9a1b69d113e62e8a295d5f5190a6010cc","datavalue":{"value":{"entity-type":"item","numeric-id":5166689,"id":"Q5166689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$402BD60D-FD0B-40E7-ABED-AF839398400F","rank":"normal"}],"P1463":[{"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":"Q2145317$EBE3AEDB-6AC9-4EA0-A2D7-B96CB8CD3167","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":"Q2145317$0E7694B0-6733-4F1D-86A2-33F8182DDC0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4b09fc0116146547cb2243374566ca9143b099b8","datavalue":{"value":{"entity-type":"item","numeric-id":25619,"id":"Q25619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$296F4460-D400-4A7D-A235-BDDBC2ECC4E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$5FA5C3BD-3A32-4FF9-A81F-AE40598747A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e3a7f5df06b272bd42f74baffc8ceda01dfacc5a","datavalue":{"value":{"entity-type":"item","numeric-id":17043,"id":"Q17043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$7C59820A-365D-4282-964E-9F3D97629E11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"33734e36764580044df2d1101af853dac96392fb","datavalue":{"value":{"entity-type":"item","numeric-id":21759,"id":"Q21759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2145317$450D8CC4-DA01-43E7-8C44-B2A2854C6386","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":"Q2145317$EC51CB1C-60FF-4671-9C9F-9D65E0936F7C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5f24b518e88c4e179298f71b39282a6e66437afb","datavalue":{"value":"https://doi.org/10.1007/978-3-030-88806-0_3","type":"string"},"datatype":"url"},"type":"statement","id":"Q2145317$B9734B24-8BA7-4192-A288-031DAA218790","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0db4d4260f2cc1e5ccefe729fa28b99775144b85","datavalue":{"value":"W3205083328","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2145317$AFD7392D-6B06-43B0-A96A-F527A8AEF7B7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b7ea57f7e0127e687d9a7284a93f39aa9309b85e","datavalue":{"value":{"entity-type":"item","numeric-id":3172934,"id":"Q3172934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5f6f765b13f8b4ffbdfed9b6c120c84ba977fa85","datavalue":{"value":{"amount":"+0.7216595411300659","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":"Q2145317$0DBF8AEF-D067-4076-A908-5C46FAED607B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"06f3820bc0abb3f731e491e70e1f9e8ddd4e7283","datavalue":{"value":{"entity-type":"item","numeric-id":5166689,"id":"Q5166689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b69e0c895073700de1f0eb9431781323b154469","datavalue":{"value":{"amount":"+0.680901825428009","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":"Q2145317$1233036A-A0F1-4802-AE4F-476A370639CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"517cd3cb617920845b81b918e3240f509e716868","datavalue":{"value":{"entity-type":"item","numeric-id":5240106,"id":"Q5240106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cf34a05b90988364ebb028827a4da607498a16d1","datavalue":{"value":{"amount":"+0.6743864417076111","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":"Q2145317$A5AA4B1A-0EB6-48DD-AA2E-689DD64142B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"76297c238e13c840da22a0b9181a5c12e41d2c5c","datavalue":{"value":{"entity-type":"item","numeric-id":1982639,"id":"Q1982639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce6f62fa9084b1d67ddf31a9bc079fb2348ac3db","datavalue":{"value":{"amount":"+0.6662790179252625","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":"Q2145317$18B204EF-28B7-482A-BDEB-74363BD46863","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb8dd5000d58f6028bd64c16a6387725ac06a8d4","datavalue":{"value":{"entity-type":"item","numeric-id":2903126,"id":"Q2903126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31a792574011a1555652b1938cc3997291658ef1","datavalue":{"value":{"amount":"+0.6658145785331726","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":"Q2145317$E313F0C9-2FEA-4D36-BA3D-91C7C72333D8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2145317","badges":[]}}}}}