{"entities":{"Q5458792":{"pageid":7488351,"ns":120,"title":"Item:Q5458792","lastrevid":101133938,"modified":"2026-06-05T23:57:41Z","type":"item","id":"Q5458792","labels":{"en":{"language":"en","value":"Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5267179"}},"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":"Q5458792$F149EC1A-6894-4722-9808-5DDC61109BD0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d4aa9fc6c7471487365d5f5acc463c613f113ef7","datavalue":{"value":{"text":"Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5458792$B145DE67-1F4A-45E1-AF32-CE6309378FD7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"08071827ab7d9fe0ab6621c90d9dfdca5406a39b","datavalue":{"value":"1134.68348","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458792$95FBA2BF-1333-4F0C-841C-C94616B845C8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b3876ed33e6cad2ecdc98a00eb854ae3c9cd4d57","datavalue":{"value":"10.1007/11506676_3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458792$0BD34D66-308A-44CC-85CB-CB8DE0FA7C98","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8deba388c1078de45653e1953b9d462190888a39","datavalue":{"value":{"entity-type":"item","numeric-id":287218,"id":"Q287218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458792$693EDA53-373A-43AF-BA38-71BEA0263A85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fd180bf3869763f3f572490f3c0f985a05a6d09f","datavalue":{"value":{"entity-type":"item","numeric-id":832223,"id":"Q832223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458792$8DD1C44C-E39F-46EC-9B53-FA2890AA6B85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"aa207266e9a1fba532940699003e04a80bb790fe","datavalue":{"value":{"entity-type":"item","numeric-id":391250,"id":"Q391250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458792$F46E61E7-D4B0-4721-8F01-87151AE8C1A1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1b30e253b497c9ae83eb323a9f6b0623853ce927","datavalue":{"value":{"entity-type":"item","numeric-id":3079910,"id":"Q3079910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458792$2116507B-1F3D-44C1-B46B-5F4780D78D1A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c1394cf050ec7558b15d2b20d30583ebe6e633ce","datavalue":{"value":{"time":"+2008-04-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5458792$346F8367-45D6-42BF-A75F-3BBF33E49FA8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458792$05F41503-5B05-4459-8974-A66370C7B5AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458792$8EFBA532-5E99-42E0-BD06-9C72310D6A78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458792$062F59B8-E70E-4D1F-90E0-F83D873D6EDB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"18c09be3fd682cd2288540a4ee06b7e557d538f6","datavalue":{"value":"5267179","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458792$75537EAC-98A4-4C51-AFFA-A44054056497","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b95a89db90765ccf45b709172ea71aa247811d25","datavalue":{"value":"Fault-tolerance","type":"string"},"datatype":"string"},"type":"statement","id":"Q5458792$EFDE1DEA-45D7-457F-80FE-A123A096FEE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q5458792$08E70720-F32C-4CBB-9F14-843EFC797177","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ce9bc06b0dfbec86650a2b13b83ea31e9af3982c","datavalue":{"value":"Program synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q5458792$3AFAD32E-5762-45A1-95DE-5BBB08848B31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f022f0315b72a5b3a5898b8e6cde2024bb232a0d","datavalue":{"value":"Program transformation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5458792$3806F266-B1E1-48E9-882D-5058FC1485F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7729cdc1ef49bcd1f402ef9250b5a2b0820b842","datavalue":{"value":"Mechanical verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5458792$11114B92-43C2-42C5-A984-6B8C4258C3D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"742acadec2058a1daf33969cf122f1e00d23a668","datavalue":{"value":"Theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5458792$1D8FC1A7-0320-4701-9F61-AF6C1F2D7E44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"63f902ec5877ba77e9585793b4cb8c66101af305","datavalue":{"value":"Addition of fault tolerance","type":"string"},"datatype":"string"},"type":"statement","id":"Q5458792$AB2C156B-ED2C-4896-A763-7B74BD54F4BF","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":"Q5458792$D635E814-A7A1-4A8F-ACCE-74E5AD8AA68A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"696f112b890c500979606d59dbdcb375105eab27","datavalue":{"value":{"entity-type":"item","numeric-id":15523,"id":"Q15523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458792$D7D9E9F5-80BE-480D-8CED-8A3BE7801417","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":"Q5458792$E639EF34-AC74-4F59-AB96-EBC6677A87A4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"09746296df8c50b2bb35612d9c4462b247f0d5fe","datavalue":{"value":"https://doi.org/10.1007/11506676_3","type":"string"},"datatype":"url"},"type":"statement","id":"Q5458792$61DBD35B-F4D1-44C4-B6BC-DA69FC8D80DD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"985f70bebe02ffbdd0523d77fe7ff59f0f81c04f","datavalue":{"value":"W2160452497","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458792$C9D3425B-C6C8-4C2A-B7EE-CF103CE6D623","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4e43a7d46e7f41a4771050849d96be1651fb6e6","datavalue":{"value":{"entity-type":"item","numeric-id":1938357,"id":"Q1938357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"526c7df2da41fa17333f62066b06c4e418e3c096","datavalue":{"value":{"amount":"+0.7604725360870361","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":"Q5458792$05D4F6A1-110C-4041-B381-862D0AEC33CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d29a5c2d083b74bc19edbd6b2c04b93cb82b32d","datavalue":{"value":{"entity-type":"item","numeric-id":5464746,"id":"Q5464746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b84e7a42688483e444d9649c6a4a1bda4a68bc42","datavalue":{"value":{"amount":"+0.747053861618042","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":"Q5458792$2DB2293C-F782-4353-BBB4-0769FC2204A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"602db440aac5dab828da4b1edbc1911f1413f4cf","datavalue":{"value":{"entity-type":"item","numeric-id":4373487,"id":"Q4373487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d4dc3cfeb514a681cb6c7738b448db29d796537","datavalue":{"value":{"amount":"+0.7468143701553345","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":"Q5458792$CE9683C0-92F1-46B0-B441-656BECA5A07A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3269fd41fbb9c2bc9830640cdb4d276df2af894d","datavalue":{"value":{"entity-type":"item","numeric-id":1330423,"id":"Q1330423"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d4dc3cfeb514a681cb6c7738b448db29d796537","datavalue":{"value":{"amount":"+0.7468143701553345","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":"Q5458792$D9D48AFE-578F-41D2-B999-D818E5555137","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07ca7f74c671f327390e0b8942a377a5d184e8e2","datavalue":{"value":{"entity-type":"item","numeric-id":555302,"id":"Q555302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa99dd5d0e02b8fc21450b8f0def7c7bcdc73e0c","datavalue":{"value":{"amount":"+0.7433125376701355","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":"Q5458792$D9415BA7-8F58-4D6C-B2FA-20B090A553F1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mechanical_Verification_of_Automatic_Synthesis_of_Fault-Tolerant_Programs"}}}}}