2026-09-23T19:52:05Zhttps://api.repository.cam.ac.uk/server/oai/requestoai:www.repository.cam.ac.uk:1810/3845142025-07-18T00:42:25Zcom_1810_219481com_1810_256065col_1810_219482
Formal Tools for Specifying Financial Smart Contracts
https://doi.org/10.17863/CAM.118487
Sorensen, Derek
0000000349376984
Madhavapeddy, Anil
Srinivasan, Keshav
Financial smart contracts routinely manage billions of US dollars worth of digital assets, and as a consequence bugs in smart contracts can be extremely costly. Because of this, much work has been done in formal verification of smart contracts to prove a contract correct with regards to its specification. However, financial smart contracts have complicated specifications, and it is not all straightforward to write one which correctly describes its intended behaviors. As a response to this challenge, we develop formal tools for specifying financial smart contracts. We target aspects of contract specification which are typically difficult to address and which can be a source of expensive contract vulnerabilities. In doing so, we hope to expand the capability of formal methods to specify desired contract behavior and thereby prevent catastrophic loss of funds.
University of Cambridge
2023-09-22
Thesis
Doctoral
Doctor of Philosophy (PhD)
eng
https://www.repository.cam.ac.uk/handle/1810/384514
https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/c53b3202-3049-4074-a956-7a6ca1bf9433/download
080ea6f0d44dcbbc77e3dd7281d059ed
https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/c43b7177-8daa-4859-b278-9fd28f30586e/download
87eda9de84448d1f82354d60eee3eb5f
http://purl.org/NET/rdflicense/allrightsreserved
blockchain
formal methods
formal verification
interactive theorem prover
smart contract verification
smart contracts