{"entities":{"Q1680264":{"pageid":1691005,"ns":120,"title":"Item:Q1680264","lastrevid":68124855,"modified":"2026-04-12T21:36:01Z","type":"item","id":"Q1680264","labels":{"en":{"language":"en","value":"Theory refinement for program verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6807236"}},"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":"Q1680264$D9ABC52B-1AC7-4392-9ADE-8A6E1AFF9E85","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"49065c8aff30d753bbc786fdd438cfd3b3506cf7","datavalue":{"value":{"text":"Theory refinement for program verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1680264$B71DD0C8-33E5-4010-B8AD-AF2D7B0EC45E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3948255e3dc981e7846fa5ba6a5deb09b82cd90d","datavalue":{"value":"1496.68191","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1680264$535B3065-F4BC-4543-98C8-04B535B4BAFC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7ec11a03dd896789dd70ed0992cce3adf1d65357","datavalue":{"value":"10.1007/978-3-319-66263-3_22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1680264$9C7BD95E-6C85-4114-80F2-59CE3E29BC9B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8ebfd430f823a6478294286ff8c6d38b91b1861a","datavalue":{"value":{"entity-type":"item","numeric-id":784138,"id":"Q784138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1680264$C1004BED-8693-4355-AFB7-E7A96B06609D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"15e7c1aedd1baa324b672c3101ff381befec47d1","datavalue":{"value":{"entity-type":"item","numeric-id":1629958,"id":"Q1629958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1680264$CDCBD70F-3681-4217-9139-98A021C42FD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"42837484d31cf34ae729e1df3cf49a1e2bca3f05","datavalue":{"value":{"entity-type":"item","numeric-id":1629957,"id":"Q1629957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1680264$3A94B5DF-6AC8-46A8-A21F-EA1714D1C544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"138e91d832e835b45e439ed8c45f97cc7963138e","datavalue":{"value":{"entity-type":"item","numeric-id":784130,"id":"Q784130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1680264$A9EA877F-25FF-4374-8255-81A883FE52E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7a7855d416a438be572c6a7aefce1c905376fea9","datavalue":{"value":{"entity-type":"item","numeric-id":233000,"id":"Q233000"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1680264$025A2535-CDC0-48F6-9984-FFCDBF81980D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"66a480d2e9b29ea82a9b0fc72873fd6d8201d31c","datavalue":{"value":{"entity-type":"item","numeric-id":287271,"id":"Q287271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1680264$3FF4E7BE-EC6E-40D0-B9D1-87D770E44F49","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5de28599599215268e07ae07176d0509363e1642","datavalue":{"value":{"time":"+2017-11-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1680264$F650B18F-0A89-450F-AE21-3A0E31F6972A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"45dbab51284644f29b0e28fed9c8cf3eb9bab43f","datavalue":{"value":"https://kclpure.kcl.ac.uk/portal/en/publications/theory-refinement-for-program-verification(f9107970-6b01-4d40-afcb-bc92984e606a).html","type":"string"},"datatype":"url"},"type":"statement","id":"Q1680264$689B7DE3-8E90-4331-9B8E-F7AC8CDAFDCF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1680264$1C8804AE-9405-46F1-BFC7-57D82B6B90E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1680264$F1A3A803-9C1F-4CFB-83C1-4BB9D7A9C59B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8a170d6b1954e9f19d751cf779a22749e0b6c3a6","datavalue":{"value":"6807236","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1680264$B158BA73-975B-43AD-8408-03A6701E5F7F","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ad41127756e7dc65bc133c87b809429e51652c7c","datavalue":{"value":"Q57699293","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1680264$172B6927-7CB9-4FC7-ADC8-D11F3D68A395","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":"Q1680264$03BB2934-49B1-4E4F-B229-5CBAC04A6E1F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a3b124e40f8fd14e2fdfa095269e30cb9beac8c1","datavalue":{"value":"W2742433495","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1680264$95814045-4FD7-414A-8281-0F8A5FB58A24","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"9736a75197a1ca8533ec219500f55511d3569410","datavalue":{"value":"conf/sat/HyvarinenAMFCS17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1680264$6ED32E3C-D4A5-4A56-A89D-BC18A802AE40","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f963c776f49a030c3643805df72eddbb99941a7f","datavalue":{"value":{"entity-type":"item","numeric-id":5222945,"id":"Q5222945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cde2b41b945c28bee89551b60eb03cc2ab01c3f9","datavalue":{"value":{"amount":"+0.7723779082298279","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":"Q1680264$8DA9DB4A-816F-4972-B7A3-F0DEF62CA67C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52121ee2bd91fb8be046c49435e9ee56268f2a38","datavalue":{"value":{"entity-type":"item","numeric-id":2225107,"id":"Q2225107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"21bfc7ebd0e8e988c6c53f05079f0b94ecd2420c","datavalue":{"value":{"amount":"+0.7568722367286682","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":"Q1680264$6A9AE317-2B6C-4DCA-B5AC-540DD81D19A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43e86e4866d63f946a9dce0ff82cf98a3b2b8ce6","datavalue":{"value":{"entity-type":"item","numeric-id":5464711,"id":"Q5464711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9b0c183a0403bfc64ca05bcb83f911ccfbb0e6e","datavalue":{"value":{"amount":"+0.753978967666626","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":"Q1680264$CC3F4CE6-734F-4DE6-808F-E12BA075702D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9bd71d433d357833a1ab35135bc0074a796311f9","datavalue":{"value":{"entity-type":"item","numeric-id":4414373,"id":"Q4414373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5133f7a8c162cf398bbd9d70d1e83fd66f128336","datavalue":{"value":{"amount":"+0.7519170045852661","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":"Q1680264$26EFE0EA-8629-4CAF-9DA3-54A046365653","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"107c509c827589280206681f81dfd6a2a3d078a8","datavalue":{"value":{"entity-type":"item","numeric-id":5168511,"id":"Q5168511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"98e1b9aed5713f91d30355d0a81bb4139084c525","datavalue":{"value":{"amount":"+0.7506375312805176","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":"Q1680264$DD43F4A5-14A5-4D6F-8608-C97504B912C9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theory refinement for program verification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Theory_refinement_for_program_verification"}}}}}