{"id":{"repo_id":"cambridge","oai_identifier":"oai:www.repository.cam.ac.uk:1810/384514"},"canonical_url":"https://search.dev.ndltd.org/etd/cambridge/oai:www.repository.cam.ac.uk:1810/384514","repository":{"repo_id":"cambridge","name":"Cambridge University","base_url":"https://api.repository.cam.ac.uk/server/oai/request"},"display":{"title":"Formal Tools for Specifying Financial Smart Contracts","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Sorensen, Derek"],"institution":"University of Cambridge","degree_name":"Doctor of Philosophy (PhD)","degree_level":"Doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Madhavapeddy, Anil","Srinivasan, Keshav"],"committee_chairs":[],"committee_members":[],"year":2023,"date_issued":"2023-09-22","date_published":"2023-09-22","updated_at":"2026-07-22T22:23:59Z","subjects":["blockchain","formal methods","formal verification","interactive theorem prover","smart contract verification","smart contracts"],"languages":["eng"],"rights":[],"rights_urls":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/c43b7177-8daa-4859-b278-9fd28f30586e/download","http://purl.org/NET/rdflicense/allrightsreserved"],"identifier_entries":[{"key":"dc:creator.authoridentifier","label":"Author Identifier","values":["0000000349376984"],"render_values":[{"text":"0000-0003-4937-6984","href":"https://orcid.org/0000-0003-4937-6984","code":true}]}]},"links":{"outbound_url":"https://doi.org/10.17863/CAM.118487","outbound_label":"DOI","outbound_source":"dc:identifier.doi"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Madhavapeddy, Anil","Srinivasan, Keshav"]},{"key":"dc:creator","label":"Author","values":["Sorensen, Derek"]},{"key":"dc:creator.authoridentifier","label":"Author Identifier","values":["0000000349376984"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.issued","label":"Date","values":["2023-09-22"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["University of Cambridge"]},{"key":"dc:relation.isreferencedby.uri","label":"Dc Relation Isreferencedby URI","values":["https://www.repository.cam.ac.uk/handle/1810/384514"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["Doctoral"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["Doctor of Philosophy (PhD)"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["blockchain","formal methods","formal verification","interactive theorem prover","smart contract verification","smart contracts"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/c43b7177-8daa-4859-b278-9fd28f30586e/download","http://purl.org/NET/rdflicense/allrightsreserved"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.doi","label":"DOI","values":["https://doi.org/10.17863/CAM.118487"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/c53b3202-3049-4074-a956-7a6ca1bf9433/download"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format.checksum.md5","label":"Dc Format Checksum Md5","values":["080ea6f0d44dcbbc77e3dd7281d059ed","87eda9de84448d1f82354d60eee3eb5f"]},{"key":"dc:title","label":"Title","values":["Formal Tools for Specifying Financial Smart Contracts"]}]}],"canonical_facts":{"dc:contributor.advisor":["Madhavapeddy, Anil","Srinivasan, Keshav"],"dc:creator":["Sorensen, Derek"],"dc:creator.authoridentifier":["0000000349376984"],"dc:date.issued":["2023-09-22"],"dc:description.abstract":["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."],"dc:format.checksum.md5":["080ea6f0d44dcbbc77e3dd7281d059ed","87eda9de84448d1f82354d60eee3eb5f"],"dc:identifier.doi":["https://doi.org/10.17863/CAM.118487"],"dc:identifier.uri":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/c53b3202-3049-4074-a956-7a6ca1bf9433/download"],"dc:language":["eng"],"dc:publisher.institution":["University of Cambridge"],"dc:relation.isreferencedby.uri":["https://www.repository.cam.ac.uk/handle/1810/384514"],"dc:rights":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/c43b7177-8daa-4859-b278-9fd28f30586e/download","http://purl.org/NET/rdflicense/allrightsreserved"],"dc:subject":["blockchain","formal methods","formal verification","interactive theorem prover","smart contract verification","smart contracts"],"dc:title":["Formal Tools for Specifying Financial Smart Contracts"],"dc:type":["Thesis"],"dc:type.qualificationlevel":["Doctoral"],"dc:type.qualificationname":["Doctor of Philosophy (PhD)"]},"updated_at":"2026-07-22T22:23:59Z"}