{"entities":{"Q6582080":{"pageid":14193236,"ns":120,"title":"Item:Q6582080","lastrevid":95581745,"modified":"2026-06-05T09:20:11Z","type":"item","id":"Q6582080","labels":{"en":{"language":"en","value":"Verification of bitcoin script in Agda using weakest preconditions for access control"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7890951"}},"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":"Q6582080$0C271B83-57F6-4C00-ADE5-2A9224A2AE99","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"31adf74657bfa5fb8ef032f1daa0d1b6146c85ac","datavalue":{"value":{"text":"Verification of bitcoin script in Agda using weakest preconditions for access control","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6582080$B37B5D53-2ECD-4C9D-92A7-2917DEDECA66","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7b0acb9dab6dce34bfa9c3911b1faa5cac4aae98","datavalue":{"value":{"entity-type":"item","numeric-id":6582078,"id":"Q6582078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6582080$EDD97387-30D2-4BB0-99C4-B7AEC6086C1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2cf66c04a9a25ec4ef5bf8b679fd619f391e2bb2","datavalue":{"value":{"entity-type":"item","numeric-id":598284,"id":"Q598284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6582080$C9F3A734-0ECB-43A8-943E-2D15D419B23D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6c05086ad770c9497243fe8ac49d476f000d6fc5","datavalue":{"value":{"entity-type":"item","numeric-id":6582079,"id":"Q6582079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6582080$DDB88DB8-58CE-4C44-BEFB-38934957E154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"726d6d17ffd7097481aaa7acac69959461b65139","datavalue":{"value":{"entity-type":"item","numeric-id":587965,"id":"Q587965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6582080$2B01AA45-223F-46BD-961B-3EFD4AD2EEFA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"93497291d8ba3cd4ceda2bd397bb8743ea86f872","datavalue":{"value":{"time":"+2024-08-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6582080$46CE3746-DC01-4903-AF8C-A5EE169634A1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6582080$2841A4C0-A2B5-4D6D-815E-0E9C1EFC080A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6582080$6AE671AE-44D8-4714-946B-3F05D382225F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"88eced2297958f6f33d6c41f0cf41dbae2b1ce0f","datavalue":{"value":"7890951","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6582080$40BABF67-A8A3-4808-B5A7-7EF327F65F50","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8f4885eaba9d3a5a82c018a8970eb9a7a2c0b387","datavalue":{"value":"blockchain","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$C276AC82-1247-4513-B8ED-8B4EFFE1F8BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d0ebf2b86f1162e75991d9f547d74ca29b5d5c88","datavalue":{"value":"cryptocurrency","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$01F76425-7E7F-4195-81E7-7D4F4271E2F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2528df059b55ae5da7c554e338e95e670e21aa7d","datavalue":{"value":"bitcoin","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$661A66C3-203D-493A-9099-AF4C25431AF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cb0249487b7eb1ecf24cddb1d300f9fa92e8fe1d","datavalue":{"value":"Agda","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$81C57365-000B-48D9-9A20-CB0FE346C171","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$36FCB078-ABFC-450D-BCFE-F446BAD930C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$013D03A4-3911-48B7-A3C3-B3120C90CDBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97e5bb7ba83dc04771289e175641dbf8abdb84ea","datavalue":{"value":"bitcoin script","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$0C66A67D-7284-43C6-A643-AC150E1F2311","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"949d03da0bd22d1f6cfd147824c9fad4c4a5b245","datavalue":{"value":"P2PKH","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$3DDD68AA-C6E9-48D8-ABD0-E2C4773BEED0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"991ac7910b1995258fa41813a9813decad91aecc","datavalue":{"value":"P2MS","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$6054F7ED-714F-4878-B291-429C386D998B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f59caf1f03985f9010aa71556abedb0a34e5f0b8","datavalue":{"value":"access control","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$0E43869C-317C-4404-9683-E974F56A603A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"26325b97ca9f91dadc7bc17af7514ea7907cb4fa","datavalue":{"value":"weakest precondition","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$E7C02811-7F37-4D59-B9B8-7B843CA9ABEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"062967b77329cd9e041ee7c06dddf47c4c9c3cc2","datavalue":{"value":"predicate transformer semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$A815C0D1-4879-4597-938A-BB768140A8B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"affe6e948030557eb5e5f18054df2fe2097360d1","datavalue":{"value":"provable correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$090AF46A-CC24-4A28-9A56-238FCB303B4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69dd490da9b67dc4fe4c624a05791d0c4fa27f2e","datavalue":{"value":"symbolic execution","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$5042DCA9-9C4C-42B6-8E93-0C7538FFC4BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ab1003dbaaaedecca41124d836f9f94d310f4e1","datavalue":{"value":"smart contracts","type":"string"},"datatype":"string"},"type":"statement","id":"Q6582080$4AD723A4-AD12-46EA-9071-28BDCC792113","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":"Q6582080$07AFA4CF-2BDE-440A-AFAC-1AB090D44E9A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c01834d2c8fb31ec7d3b78737ccf55290a19f5d5","datavalue":{"value":"10.4230/LIPICS.TYPES.2021.1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6582080$63952E20-9CE7-44DC-A014-4FCADD9D58B5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verification of bitcoin script in Agda using weakest preconditions for access control","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verification_of_bitcoin_script_in_Agda_using_weakest_preconditions_for_access_control"}}}}}