SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand

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 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:30
Session 3: Applications of Formal MethodsFTSCS at Seminar Room LG004
15:30
30m
Talk
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
30m
Talk
Formal Probabilistic Risk Assessment of a Nuclear Power PlantVirtual
FTSCS
Mohamed Abdelghany Concordia University, Sofiene Tahar Concordia University
DOI
16:30
30m
Talk
Modelling a Blockchain for Smart Contract Verification using DeepSEAIn Person
FTSCS
Daniel Britten University of Waikato, Steve Reeves University of Waikato
DOI
17:00
30m
Talk
Towards a Formalization of the Active Corner Method for Collision Avoidance in PVSIn Person
FTSCS
Nishant Kheterpal University of Michigan, Jean-Baptiste Jeannin University of Michigan at Ann Arbor