Verifying liquidity of recursive bitcoin contracts

MaRDI QIDQ5028478zbMATH OpenFDO

Authors Massimo Bartoletti, Stefano Lande, Maurizio Murgia, Roberto Zunino

Publication date 9 February 2022

Full work available at URL https://arxiv.org/abs/2011.14165, https://lmcs.episciences.org/9031

zbMATH Keywords

BitcoinBitMLblockchainliquiditysmart contractsverification

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Formal verification of fair exchange based on Bitcoin smart contracts
• Verification-Led Smart Contracts
• EthVer: formal verification of randomized Ethereum smart contracts
• Modeling Bitcoin contracts by timed automata
• Quantitative analysis of smart contracts

Cites work

• How to use bitcoin to design fair protocols
• Modeling Bitcoin contracts by timed automata
• Modelling and verifying contract-oriented systems in Maude

Cited in

(3)

• Certifying Findel derivatives for blockchain
• Liquidity analysis in resource-aware programming
• DeFi composability as MEV non-interference

Describes a project that uses

Uses Software

• GitHub

This page was built for publication: Verifying liquidity of recursive bitcoin contracts

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