Verification of bitcoin script in Agda using weakest preconditions for access control

DOI10.4230/LIPICS.TYPES.2021.1MaRDI QIDQ6582080zbMATH OpenFDO

Authors Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, Anton Setzer

Publication date 1 August 2024

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2021.1

zbMATH Keywords

access controlAgdabitcoinbitcoin scriptblockchaincryptocurrencyHoare logicP2MSP2PKHpredicate transformer semanticsprovable correctnesssmart contractssymbolic executionverificationweakest precondition

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

This page was built for publication: Verification of bitcoin script in Agda using weakest preconditions for access control

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6582080)