{"entities":{"Q2517836":{"pageid":2528579,"ns":120,"title":"Item:Q2517836","lastrevid":50535422,"modified":"2026-01-14T07:58:08Z","type":"item","id":"Q2517836","labels":{"en":{"language":"en","value":"Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5488582"}},"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":"Q2517836$69B455C6-8047-4F5E-B441-02A40E2C82CB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"49e40a378d554027322fd196301f66bc7296c7ca","datavalue":{"value":{"text":"Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2517836$563599AC-10CA-4A7C-B924-FD800C8A4982","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0239bbe380b8184ec78133af875fd33fd5233a7c","datavalue":{"value":"1159.68022","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2517836$810F5F4A-B273-4986-BA4E-4092044261FF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c24c5c5cceb777d2d5d5c94a9c58cfc4129afdd4","datavalue":{"value":{"entity-type":"item","numeric-id":2517835,"id":"Q2517835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2517836$D1E0D36D-5B8F-4CF8-BBF7-28834036E27F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4082512e7d3530b9726df691c7c28e9fec542a8c","datavalue":{"value":{"entity-type":"item","numeric-id":169675,"id":"Q169675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2517836$A6F063F7-3828-4CB9-AEA6-4F581BA3C457","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"40eec35cc4088460d56a8604f6511af334349525","datavalue":{"value":{"time":"+2009-01-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2517836$38BE2B6F-64C4-4AE5-BC25-A921101A5ED3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2517836$EC311D9C-1CDB-4209-AE94-12C9F5A1E119","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b3f5570531d36cdad95fcc8cba24a2dabc5fbbbf","datavalue":{"value":"94A60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2517836$E261D539-2BB5-4F31-B5DD-82EF8FD6D1B8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1ff844ed163e0ae595e30f24f08fbabbb3642037","datavalue":{"value":"5488582","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2517836$03B23ECC-5AC1-4D35-BE07-3778FBB282F4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2517836$272B742D-11CC-4F65-B868-A2FF049C2AF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"73b4c65f1932723e758d611f0e45f29f11ae5669","datavalue":{"value":"probability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2517836$F46A762B-D9EA-42DE-A326-8F7E7AAB76B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c4978f2c4d263ef258ed0ffc576a325d510c4d8","datavalue":{"value":"axiomatization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2517836$1BB4578D-604C-48CC-92D9-E8C8A00EAFB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d54d97c9d74a7974164bd27bc3725f50a6bd71c8","datavalue":{"value":"cryptography","type":"string"},"datatype":"string"},"type":"statement","id":"Q2517836$C41865C2-F35E-44AF-8110-C8FEA55CB9F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"affe6e948030557eb5e5f18054df2fe2097360d1","datavalue":{"value":"provable correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q2517836$5527604A-299D-411B-B8AD-2A53E3B66D10","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2517836$E8CF49B5-883D-47A9-8D83-0B9BC307B215","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":"Q2517836$6EDF2A20-C6A6-44FC-A94D-5DE659042D37","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6fbe193773cef3ad3257fdc193720c9e39430669","datavalue":{"value":"https://doi.org/10.1016/j.scico.2008.09.006","type":"string"},"datatype":"url"},"type":"statement","id":"Q2517836$67726F54-E807-4022-A3BB-CCD65106BD7C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fbe4ab779dab2357b12eb88b98500ea10425ecba","datavalue":{"value":"W2145188057","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2517836$B7E76BAB-5E76-49E5-B1CD-FBC48329CC5C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"524c83798d83bbbf12f5c71ac493341e47477925","datavalue":{"value":"10.1016/J.SCICO.2008.09.006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2517836$D5DA3982-BCE8-42C9-91E8-14DFB1BE7C77","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a9c86cfed88d5372ed769eef3623b1170b13d18","datavalue":{"value":{"entity-type":"item","numeric-id":3591439,"id":"Q3591439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96f4606667969817926d844f6d8de29f6bde1c19","datavalue":{"value":{"amount":"+0.845404326915741","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":"Q2517836$20552B0E-81E7-451D-A4B1-419B960CA2C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5cadaf031c9fd85e583aad9ed7daf3b5d8afe4a5","datavalue":{"value":{"entity-type":"item","numeric-id":5261508,"id":"Q5261508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e97ef03ba92322a6379b39a3eb3996e0a7d6bfaa","datavalue":{"value":{"amount":"+0.7989811897277832","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":"Q2517836$5A791F95-2F38-4EF7-A6C1-163C12C010C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b3a30adc631633b6c03d9642b0a683d85bf099a5","datavalue":{"value":{"entity-type":"item","numeric-id":2908554,"id":"Q2908554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0e8f55bf71e0df87830e50bc2eee92a95e5d2d88","datavalue":{"value":{"amount":"+0.7629608511924744","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":"Q2517836$0B5BBEDC-78DC-4A94-9105-0B61FEA4C6CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ccba59ae8d5dbfac518b4d3720026f53bca440e4","datavalue":{"value":{"entity-type":"item","numeric-id":4314048,"id":"Q4314048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ad4bd9016b7aedea77306df4e344211924a1785d","datavalue":{"value":{"amount":"+0.7546668648719788","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":"Q2517836$C17F2D1D-6BF1-48D4-8288-48901674ADA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1aa4625440697f2ee72d406a46d1e48df0580662","datavalue":{"value":{"entity-type":"item","numeric-id":2914729,"id":"Q2914729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"359fd244bd88ddd37e653766a5fdcde7dc74d479","datavalue":{"value":{"amount":"+0.7400735020637512","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":"Q2517836$C79BE7DC-A3E8-460C-9D31-1F890FEEC5AA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2517836","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2517836"}}}}}