{"entities":{"Q604381":{"pageid":606157,"ns":120,"title":"Item:Q604381","lastrevid":51128225,"modified":"2026-01-16T20:06:02Z","type":"item","id":"Q604381","labels":{"en":{"language":"en","value":"Mechanical inference of invariants for FOR-loops"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5814767"}},"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":"Q604381$DD80D748-AB6C-4390-938A-EDC1089CEA14","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"15186d45002bb3b114d93a120b8249cec02e4812","datavalue":{"value":{"text":"Mechanical inference of invariants for FOR-loops","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q604381$D280303C-C268-45FA-BFF7-A78533974B93","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1c1bb0a7d39f16dac4e1e319b56ee877a522116b","datavalue":{"value":"1208.68147","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q604381$9C718B3A-20E7-47A9-AB4A-C606C40C9897","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c0cbf2c4cfca3803cd6819fbaed7f1bb567ef4c6","datavalue":{"value":{"entity-type":"item","numeric-id":604379,"id":"Q604379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$9E6C18CD-D1E7-4D14-AA5E-79FB4B602D4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e3b7be2006956c8183dcfd17d471622f6d0d8156","datavalue":{"value":{"entity-type":"item","numeric-id":604380,"id":"Q604380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$957351A1-E6BB-46ED-9A0B-2B8C20376DBF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$9B2CA9D0-CB9B-4E28-8DD9-019572F883CA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c9ea9622d88fa8ef1a3077c0b305abfad406e986","datavalue":{"value":{"time":"+2010-11-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q604381$33FF0014-F59B-4804-9309-2F193697C3A8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q604381$300611C3-B67A-42C5-B564-5775E8D8B5E6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"eda5b9649dfa83462c91d154efa5fd7f56a0626b","datavalue":{"value":"5814767","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q604381$D9728869-6E2B-4E47-91E8-654B2134DEA0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"033bcb9864019192358d248f1765aefb1c4f7385","datavalue":{"value":"mechanical verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q604381$E7615C39-54FA-4D55-84DA-3A37460101CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cbd7ce168f23f4489c2fc1869c0da63f30235ab5","datavalue":{"value":"mechanical inference of loop invariants","type":"string"},"datatype":"string"},"type":"statement","id":"Q604381$73871111-B53C-4250-BBEA-FB7156FC68B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"148b140237f7dbe619d09cf76cefe5377520c8a3","datavalue":{"value":"FOR-loop","type":"string"},"datatype":"string"},"type":"statement","id":"Q604381$D4B35DF2-8F5E-4F91-A20C-7AAD6E5412F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7bffac4f6e54ad43493b5d1ebc5393c1f7606358","datavalue":{"value":"RCPV","type":"string"},"datatype":"string"},"type":"statement","id":"Q604381$3FBC904B-F275-48B0-8512-6339F36A8AAC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"12b8fef36068e5bdaa4e8c4c10a706c6f98b9349","datavalue":{"value":{"entity-type":"item","numeric-id":21946,"id":"Q21946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$1684906D-51D7-4D62-B65C-6BD11D097D75","rank":"normal"},{"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":"Q604381$B9863870-B5C7-4025-93FF-38D5131A6CC2","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":"Q604381$157777F2-3598-4151-83CC-D98C2EF927FF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"63cd12a15ad23ced8e08b1a0a698c4223d050c2b","datavalue":{"value":"https://doi.org/10.1016/j.jsc.2008.11.008","type":"string"},"datatype":"url"},"type":"statement","id":"Q604381$88B4A8D9-1BC6-4066-A614-AD04B13F07C9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d57e85e322a727eed326b908886367dfaa59cf8f","datavalue":{"value":"W2035919470","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q604381$7808F730-0A45-4C7F-8060-A03F1EC743E8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"61ec63bea625b06509e4372389dbe27861ae44d0","datavalue":{"value":{"entity-type":"item","numeric-id":4343983,"id":"Q4343983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$3E696101-78C3-4D07-9014-C2AA1EF944A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e681342f87eb45209d54d8ef45b550c76a8592f","datavalue":{"value":{"entity-type":"item","numeric-id":3868727,"id":"Q3868727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$F625BE99-7225-47FD-A0F4-E0ED4DD7254C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"226149966044b48001c0682076573b6d91099455","datavalue":{"value":{"entity-type":"item","numeric-id":4773988,"id":"Q4773988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$4369FF6D-F26D-4F07-9DA3-1932D72498F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd265bdbcf41f2b9982b655d7aaf44e4072217fa","datavalue":{"value":{"entity-type":"item","numeric-id":4692630,"id":"Q4692630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$FCB63DE6-E4A0-4C55-B915-F62F80423F1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b4c1575390a21dabffd80a0444998afabd82bc71","datavalue":{"value":{"entity-type":"item","numeric-id":3321419,"id":"Q3321419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$234470DE-131A-4943-9AD8-C0C7204B7E77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4214dfeddf653cbc97d67a6b624378d98101965e","datavalue":{"value":{"entity-type":"item","numeric-id":3914404,"id":"Q3914404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$AFD43A53-5329-4EDD-AAF5-B89A36EBEEF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af9e098165be5a6ce3b6b51665cbf6a402547015","datavalue":{"value":{"entity-type":"item","numeric-id":4023189,"id":"Q4023189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$060DEE81-BA1A-4BFD-84BB-54173F26E9FB","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":"Q604381$F224420B-5669-4F25-A95B-DBDF324E9B75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6130a72bad290e99b4d30823cf592f64ef05b4a8","datavalue":{"value":{"entity-type":"item","numeric-id":5584402,"id":"Q5584402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$1C453216-847D-4652-98F4-98A7F635FA36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8eb2bf873d9014924c1ae83ac7088d5fb1f4aad","datavalue":{"value":{"entity-type":"item","numeric-id":4692507,"id":"Q4692507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$E8E1C7AC-DFFF-482F-AE52-6943F8AAAB64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"826f27ba8fd990b10810e9d860feb46027482551","datavalue":{"value":{"entity-type":"item","numeric-id":1052815,"id":"Q1052815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$61BDE403-EDEB-4B5B-8320-F88FC0B58A84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"02b52a1a8124add92823b9e50e481a0f7868cd92","datavalue":{"value":{"entity-type":"item","numeric-id":1285784,"id":"Q1285784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$19729D66-12F3-4B83-86F6-26BDDDEDFB4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$ED4FBD64-4769-43D5-A164-5CF0F10FF830","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"530a0088eab2b772913687ffac9402800499441a","datavalue":{"value":{"entity-type":"item","numeric-id":5659054,"id":"Q5659054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$59E8FE91-B4D9-408F-8EF6-FE6192FA4211","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d83e0d809c9946be35cf8127887d0a3709fa8a8","datavalue":{"value":{"entity-type":"item","numeric-id":4124273,"id":"Q4124273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$DA4BAF6B-8D3F-4AF8-9972-E75412D86466","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"817a925eb5294986b9f403eea65fb6d1c9bdaaa9","datavalue":{"value":{"entity-type":"item","numeric-id":797985,"id":"Q797985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$EEF8AA12-B649-46E0-809B-D026A90EB83F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07a293cf8e11c98f47912c198c41ec9b7a2a6925","datavalue":{"value":{"entity-type":"item","numeric-id":4174210,"id":"Q4174210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$14060324-C385-4817-B4BA-8B197819DE1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ae8d4019bbc3963780842028820817d531f0c4a","datavalue":{"value":{"entity-type":"item","numeric-id":4120116,"id":"Q4120116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$06958983-A55E-47A7-9400-169E099227E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70900c3b4b31a6363b51a557b0533917f6773240","datavalue":{"value":{"entity-type":"item","numeric-id":2390319,"id":"Q2390319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$27F83FE8-E17A-4BEA-9C7D-5E136A46B146","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c89dbab3e6b723e605c6aa70dd1a0838f12ee2f","datavalue":{"value":{"entity-type":"item","numeric-id":859956,"id":"Q859956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$5B8D7477-B184-4106-9B67-7B55087C850F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d65f6021ee8a90d0397d10405ca987700f008fae","datavalue":{"value":{"entity-type":"item","numeric-id":3868729,"id":"Q3868729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$3D2E013B-4F22-47D3-A1E2-9E99FB97B85D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"613255b4bb6fd411409fb47c605997cb9ba28d51","datavalue":{"value":{"entity-type":"item","numeric-id":5180828,"id":"Q5180828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q604381$4926A147-5DE7-4F0B-8E9D-298A698A9DCB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6cab6dc9742416b7845436fdd5b1a341b100efda","datavalue":{"value":"10.1016/J.JSC.2008.11.008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q604381$6EDFAEBD-4CBD-4F84-8A0B-BDD13C09FF3A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b9d15a4143f1d4649ec9a4d200a83aa195298d12","datavalue":{"value":{"entity-type":"item","numeric-id":1322851,"id":"Q1322851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b9da9c7ae867be7f5f1ab4e8ae121ca0a4e426d","datavalue":{"value":{"amount":"+0.8046083450317383","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":"Q604381$D7A2C286-58C5-494B-9DCA-61A0457D70A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e36f3694c49ffa7483df2a818342d806f5dea076","datavalue":{"value":{"entity-type":"item","numeric-id":5740643,"id":"Q5740643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d925133d3646a6819cd1a8cab24bfc31acb5101","datavalue":{"value":{"amount":"+0.8012889623641968","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":"Q604381$17CB10B5-D17F-4B42-98C9-B23D66ED8D95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0605ef596d929245fcfc8a407c55f9f17fb78984","datavalue":{"value":{"entity-type":"item","numeric-id":3586008,"id":"Q3586008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6777a6dbbd7d5cbcf041a752d76982bb0b4d7b63","datavalue":{"value":{"amount":"+0.7929205298423767","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":"Q604381$40E460F2-9EBC-4E88-9261-E9EE2F776687","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5cb23bd8c9cdca6792eabcff20647876a470cc75","datavalue":{"value":{"entity-type":"item","numeric-id":5096093,"id":"Q5096093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"189b07ecc60200d2d3e722e0dc647c395c55e448","datavalue":{"value":{"amount":"+0.7648380398750305","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":"Q604381$9AC60BF8-83D7-4F3E-9792-F344AE243BC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cba91a2fa8a38f05d02fe6a811450a3326020603","datavalue":{"value":{"entity-type":"item","numeric-id":5176169,"id":"Q5176169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36f6135a6da4656d282bd5979744c63bbc173fd4","datavalue":{"value":{"amount":"+0.7589530348777771","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":"Q604381$36B17D13-7FDC-4731-8DF0-C44BD10A5C94","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:604381","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:604381"}}}}}