Towards an Implementation of Differential Dynamic Logic in PVSvirtual
Tue 14 Jun 2022 23:20 - 23:45 at Boardroom - Paper Session 1
This paper describes an ongoing effort to embed and verify Differential Dynamic Logic (DDL) in the Prototype Verification System (PVS). DDL is a logic for specifying and formally reasoning about hybrid systems, which employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of DDL in PVS offers an independent formal verification of the semantics and rules of DDL. Second, the embedding is fully operational within PVS, giving users of PVS the ability to use DDL in the formal specification and verification process. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on DDL objects. In addition to the embedding and verification of DDL, a custom extension for Visual Studio Code has been developed, so that a stylized DDL syntax can be used to specify hybrid programs and their properties.
Tue 14 JunDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | Paper Session 1 SOAP at Boardroom +12h Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL All papers will be allocated a time slot of 25 min (20min talk + 5 min questions) | ||
10:30 25mTalk | Abstract interpretation of Michelson smart-contracts SOAP P: Guillaume Bau , Antoine Miné Sorbonne Université, Vincent Botbol Nomadic Labs, Mehdi Bouaziz Nomadic Labs Paris | ||
10:55 25mTalk | BinFPE: Accurate Floating-Point Exception Detection for GPU Applications SOAP P: Ignacio Laguna Lawrence Livermore National Laboratory, Xinyi Li University of Utah, Ganesh Gopalakrishnan University of Utah | ||
11:20 25mTalk | Towards an Implementation of Differential Dynamic Logic in PVSvirtual SOAP P: J Tanner Slagel , César Muñoz NASA Langley Research Center, Swee Balachandran National Institute of Aerospace, Mariano Moscato National Institute of Aerospace, Aaron Dutle NASA Langley Research Center, Paolo Masci National Institute of Aerospace, USA, Lauren White NASA Langley Research Center | ||
11:45 25mTalk | Statically Detecting Data Leakages in Data Science Codevirtual SOAP | ||
22:30 - 00:00 | |||
22:30 25mTalk | Abstract interpretation of Michelson smart-contracts SOAP P: Guillaume Bau , Antoine Miné Sorbonne Université, Vincent Botbol Nomadic Labs, Mehdi Bouaziz Nomadic Labs Paris | ||
22:55 25mTalk | BinFPE: Accurate Floating-Point Exception Detection for GPU Applications SOAP P: Ignacio Laguna Lawrence Livermore National Laboratory, Xinyi Li University of Utah, Ganesh Gopalakrishnan University of Utah | ||
23:20 25mTalk | Towards an Implementation of Differential Dynamic Logic in PVSvirtual SOAP P: J Tanner Slagel , César Muñoz NASA Langley Research Center, Swee Balachandran National Institute of Aerospace, Mariano Moscato National Institute of Aerospace, Aaron Dutle NASA Langley Research Center, Paolo Masci National Institute of Aerospace, USA, Lauren White NASA Langley Research Center | ||
23:45 25mTalk | Statically Detecting Data Leakages in Data Science Codevirtual SOAP | ||