{"entities":{"Q832320":{"pageid":834168,"ns":120,"title":"Item:Q832320","lastrevid":57687294,"modified":"2026-03-31T22:11:57Z","type":"item","id":"Q832320","labels":{"en":{"language":"en","value":"\\textsc{Diffy}: inductive reasoning of array programs using difference invariants"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7498213"}},"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":"Q832320$C54F694B-4006-4EE6-9B51-C1E7117696BD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d0f7cd8e1b75bfec7996fa8ceebc62b4d74e8b9e","datavalue":{"value":{"text":"\\textsc{Diffy}: inductive reasoning of array programs using difference invariants","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q832320$001884D2-0914-4E10-BBF2-4DC35DE2EC90","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"36725b3ef6d834a3fc800eff7950192234ae0ae4","datavalue":{"value":"1493.68101","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832320$B13907F8-3F3F-4E80-A3D4-25A28A99050C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8167bb3e05a6dca8d9cb8badd59838311008255b","datavalue":{"value":"10.1007/978-3-030-81688-9_42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832320$9B2F4010-7CED-4946-8BE1-49A30C93AEF5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9402163f6499a1d088bfc900c18810df19851ad9","datavalue":{"value":{"entity-type":"item","numeric-id":526772,"id":"Q526772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$6A73AC9C-A79F-4F9E-8001-6F42F3CA8350","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cefe2994cd2e378e79e344a451c126379a495f1d","datavalue":{"value":{"entity-type":"item","numeric-id":630709,"id":"Q630709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$9177643F-39B8-471E-8298-2C04051EADDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a229c5eba8b458580a3a543442fd24f0e965fc2d","datavalue":{"value":{"entity-type":"item","numeric-id":832319,"id":"Q832319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$2D4C26C4-CB39-493A-912C-110190A283CB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"26426ab4d5a6ecfa201abc41ba9257e3996155a5","datavalue":{"value":{"time":"+2022-03-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q832320$657456C8-19B5-4368-B6B5-9CA7FFCE5272","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6c8f0f0e9800896ddee95aa7b3788d2661675bb0","datavalue":{"value":"https://arxiv.org/abs/2105.14748","type":"string"},"datatype":"url"},"type":"statement","id":"Q832320$06F67C36-FFBA-47C8-83C4-E5D5ECDF3724","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832320$809851C3-03BA-4B94-8555-A48B2A960F4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832320$076BD828-3868-40CE-9BDB-ADE391543542","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6ae6ecfb1d08d5d3500c179c4aa4daf2c40e0bf8","datavalue":{"value":"7498213","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832320$B8A53177-A4BD-4CE3-8420-25121C1D7C7C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fedb99aafb4892a69662c5ebaffc64ecb6451370","datavalue":{"value":{"entity-type":"item","numeric-id":16326,"id":"Q16326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$A9BC00C5-BBF0-457D-9770-B7F9C8E7CD29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"edcc5b773aefa12179daf9a302ebafdcfbdfdca6","datavalue":{"value":{"entity-type":"item","numeric-id":25620,"id":"Q25620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$1E8F235E-D186-4E6F-BFE0-C8454CAFE435","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dd73c0a588eca90d6b4027348c417905031d8d73","datavalue":{"value":{"entity-type":"item","numeric-id":33279,"id":"Q33279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$7DD5CF1F-021C-4316-B4DD-23A099FB0591","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":"Q832320$3754CF59-500E-4E47-8D4A-C6C4620E5F69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"71b79027a4b3c3d7cd60462ef3801c42871145ae","datavalue":{"value":{"entity-type":"item","numeric-id":45000,"id":"Q45000"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$8DD827F6-C581-464D-8638-1494DB1105ED","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":"Q832320$59A926F4-6E99-4187-ADE5-8367CF23E529","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"99a07654c65444a050062ac8472703cb98630569","datavalue":{"value":"W3183515470","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832320$58A5AE4A-E4FB-435D-B828-FA5D639E27C3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a257ff0958ba2ab18651e0ae0e647b82a1a678f","datavalue":{"value":{"entity-type":"item","numeric-id":2891439,"id":"Q2891439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$EC5F8F5E-2961-4B93-9D29-D607691862DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f176d988fabbd626744eee2651f4ef8cf9c0825f","datavalue":{"value":{"entity-type":"item","numeric-id":3457775,"id":"Q3457775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$50B0DDCD-1DE2-438F-AB96-167641719E9F","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":"Q832320$ABABCEAA-CC62-4C26-B7A2-17AEC77D2C4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62182dcb51c15de8e9697db383dc1581d8b46dcc","datavalue":{"value":{"entity-type":"item","numeric-id":3583851,"id":"Q3583851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$3C96F625-9ECA-4921-99E0-EC84DC971CC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f5ebbea66cbe10132be316b761463856b5e5791","datavalue":{"value":{"entity-type":"item","numeric-id":5233256,"id":"Q5233256"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$80736DB8-01B4-4E23-BD3C-78C6CFBC7FF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a45a7b50e50bf157610c2a1c3931ec79fd87b09a","datavalue":{"value":{"entity-type":"item","numeric-id":5039501,"id":"Q5039501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$2C670BE6-CFEF-4C33-BF0C-667F9BB755FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd1f487f894ada316ae2893024e29e29b624b634","datavalue":{"value":{"entity-type":"item","numeric-id":5408536,"id":"Q5408536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$C99FC9E9-E5E3-483E-B86D-463C9B6FFABA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85ed5493d80478a3f1c5f7d6db27292dafc6a2c6","datavalue":{"value":{"entity-type":"item","numeric-id":453505,"id":"Q453505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$0FAD7907-153A-404D-8159-DB5CE91AE00C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"774e07bf0cdbe35003eaaf8e3d497ff9f1ce6b06","datavalue":{"value":{"entity-type":"item","numeric-id":6194577,"id":"Q6194577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$0BCEE891-1E25-49FE-B7B5-E34E921D62F7","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":"Q832320$655EF1C1-9130-41CC-8DFD-8BBE50852085","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd7518c3dc697c1f88392c573900510e6c347126","datavalue":{"value":{"entity-type":"item","numeric-id":5276157,"id":"Q5276157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$155847BC-DCAB-42B5-A37C-E9FA5081285D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66ad83169ed8389564075d9eacd3961be1c6400d","datavalue":{"value":{"entity-type":"item","numeric-id":3189843,"id":"Q3189843"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$8A9FC3DB-ED67-44AE-A6FF-B6FB35129F47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd51bbb96625374ba0527eef6fa500f596e78094","datavalue":{"value":{"entity-type":"item","numeric-id":6109591,"id":"Q6109591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$83CD1D1B-3816-4F4C-AA2D-94203A8AAB56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"233fc4b17b1af3434fc767d2e3e5cfddfad5ad78","datavalue":{"value":{"entity-type":"item","numeric-id":784119,"id":"Q784119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$2A8900E1-02D7-49C2-9B63-057273A6EF11","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":"Q832320$9BC9DAC3-99B1-4290-A25A-188EEC859583","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9d0dd7bb6db6a4c0ce328175c5c1c2e0bc50527","datavalue":{"value":{"entity-type":"item","numeric-id":5429322,"id":"Q5429322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$4CE3472C-FC4C-44D2-BFD8-D3838D235307","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04b849a03e9166716352f85f235b1816d320391e","datavalue":{"value":{"entity-type":"item","numeric-id":274400,"id":"Q274400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$FE69D7A5-5720-4C07-8B91-4C8C7F286457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33b8ed770b8d245384879223baff02e99d04132b","datavalue":{"value":{"entity-type":"item","numeric-id":5172648,"id":"Q5172648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$E527AA60-6A5E-4728-81C1-7D8B0896BC34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb3d973ee67a0d57722d1373dad12c99bf3d07ce","datavalue":{"value":{"entity-type":"item","numeric-id":2044196,"id":"Q2044196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$5F2E61D4-B023-4005-9196-AAD76F535268","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7e7a69944a208912cc786a2c8236ca37bc32116","datavalue":{"value":{"entity-type":"item","numeric-id":1664399,"id":"Q1664399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$6AC3FD56-6FE7-4D78-B7DF-D5C5FA828346","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d6d6f89901bb1264c7e9f22a16224fb694fab3c0","datavalue":{"value":{"entity-type":"item","numeric-id":3943982,"id":"Q3943982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$F7D3AEE2-8F07-40D7-88B6-EB67F2E9413D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2eebb6c8c7f52075680b76433c15aab3dfaf824b","datavalue":{"value":{"entity-type":"item","numeric-id":2848907,"id":"Q2848907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$E07D4BB6-D46C-40C5-A34A-81BB43AE8253","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3b3a3f4b3f44b312014bf38e16d46d1bd8aea8c","datavalue":{"value":{"entity-type":"item","numeric-id":5716568,"id":"Q5716568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832320$3B16F859-C4E3-40AD-BF13-595165849A60","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ade7e9871d3b7237ee26a5d7af7fab4ebaecb5e","datavalue":{"value":{"entity-type":"item","numeric-id":5039501,"id":"Q5039501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25bba3e4ceebeab268374cd1f585a294885fbf7a","datavalue":{"value":{"amount":"+0.7763860821723938","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":"Q832320$C14AD496-1C0B-4232-AB80-EB142BBDCE8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5563b95faa1b44f2d752ed5cbaa7a33e4344ac20","datavalue":{"value":{"entity-type":"item","numeric-id":3636859,"id":"Q3636859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"be583c98131281a45d31c78e2e758ab95a3f94aa","datavalue":{"value":{"amount":"+0.7169774770736694","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":"Q832320$F7753BBB-A756-4371-B895-F84309B81077","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52f8ea1e808d67e60c7597974a18e0ac160aa143","datavalue":{"value":{"entity-type":"item","numeric-id":2324216,"id":"Q2324216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"52083e405437f7a8e9023483898b9c5770f3ffae","datavalue":{"value":{"amount":"+0.7012413740158081","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":"Q832320$0F1DA098-ABB9-4C05-ADCB-4F4BF62E5098","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4f9550b460f7de999a0525aec28440b36da166a0","datavalue":{"value":{"entity-type":"item","numeric-id":5233256,"id":"Q5233256"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8fdf4f901b2ddff08da41f4715bb8b08c47fd31","datavalue":{"value":{"amount":"+0.7009531259536743","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":"Q832320$5D8CEEC9-C909-43E8-BB8F-CCA3EAA5E61D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7080246487054104b638d53769ec9526e92f5c50","datavalue":{"value":{"entity-type":"item","numeric-id":5429322,"id":"Q5429322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f7647c4543d50b0033f3069da02488694dd8a19","datavalue":{"value":{"amount":"+0.6969573497772217","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":"Q832320$DED96CF7-B1F1-43BD-A267-028EB69DE04E","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":"Q832320$6AF82147-6667-4F8F-9021-31C7007B6A9A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:832320","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:832320"}}}}}