SPLASH 2022 (series) / FTSCS 2022 (series) / Formal Techniques for Safety-Critical Systems / Modelling a Blockchain for Smart Contract Verification using DeepSEA
Modelling a Blockchain for Smart Contract Verification using DeepSEAIn Person
Wed 7 Dec 2022 16:30 - 17:00 at Seminar Room LG004 - Session 3: Applications of Formal Methods
To create trustworthy programs, the 'gold standard' is specifications at a high-enough level to clearly correspond to the informal specifications, and also a refinement proof linking these high-level specifications down to, in our case, executable bytecode. The DeepSEA system demonstrates how this can be done, in the context of smart contracts on the Ethereum blockchain. A key component of this is the model of the blockchain on which the smart contracts reside. When doing proofs in DeepSEA, it is critical to have such a model, which allows for the writing of specifications at a high-level clearly corresponding to informal specifications. A candidate model for doing so and its usefulness for carrying out proofs is discussed in this paper.
Wed 7 DecDisplayed time zone: Auckland, Wellington change
Wed 7 Dec
Displayed time zone: Auckland, Wellington change
15:30 - 17:30 | |||
15:30 30mTalk | Synchronous Programming and Refinement Types in Robotics: From Verification to ImplementationIn Person FTSCS Jiawei Chen University of Michigan at Ann Arbor, José Luiz Vargas de Mendonça University of Michigan at Ann Arbor, Shayan Jalili University of Michigan at Ann Arbor, Bereket Shimels Ayele Addis Ababa Institute of Technology, Bereket Ngussie Bekele Addis Ababa Institute of Technology, Zhemin Qu University of Michigan at Ann Arbor, Pranjal Sharma University of Michigan at Ann Arbor, Tigist Shiferaw Addis Ababa Institute of Technology, Yicheng Zhang University of Michigan at Ann Arbor, Jean-Baptiste Jeannin University of Michigan at Ann Arbor DOI | ||
16:00 30mTalk | Formal Probabilistic Risk Assessment of a Nuclear Power PlantVirtual FTSCS DOI | ||
16:30 30mTalk | Modelling a Blockchain for Smart Contract Verification using DeepSEAIn Person FTSCS DOI | ||
17:00 30mTalk | Towards a Formalization of the Active Corner Method for Collision Avoidance in PVSIn Person FTSCS |