Write a Blog >>
ICSE 2023
Sun 14 - Sat 20 May 2023 Melbourne, Australia
Wed 17 May 2023 14:30 - 14:45 at Meeting Room 110 - Program translation and synthesis Chair(s): Andy Zaidman

Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to automation of formal proofs of safety in hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.

Wed 17 May

Displayed time zone: Hobart change

13:45 - 15:15
Program translation and synthesisTechnical Track / Showcase / NIER - New Ideas and Emerging Results at Meeting Room 110
Chair(s): Andy Zaidman Delft University of Technology
13:45
15m
Talk
Concrat: An Automatic C-to-Rust Lock API Translator for Concurrent Programs
Technical Track
Pre-print
14:00
15m
Talk
Triggers for Reactive Synthesis Specifications
Technical Track
Gal Amram Tel Aviv University, Dor Ma'ayan Tel Aviv University, Shahar Maoz Tel Aviv University, Or Pistiner Tel Aviv University, Jan Oliver Ringert Bauhaus-University Weimar
Pre-print
14:15
15m
Talk
Using Reactive Synthesis: An End-to-End Exploratory Case Study
Technical Track
Dor Ma'ayan Tel Aviv University, Shahar Maoz Tel Aviv University
Pre-print
14:30
15m
Talk
Pegasus: A Framework for Sound Continuous Invariant Generation
Showcase
Andrew Sogokon , Stefan Mitsch Carnegie Mellon University, USA, Yong Kiam Tan Carnegie Mellon University, Katherine Kosaian CMU, Carnegie Mellon University, André Platzer Karlsruhe Institute of Technology (KIT)
14:45
7m
Talk
On ML-Based Program Translation: Perils and Promises
NIER - New Ideas and Emerging Results
Aniketh Malyala Yale University, Katelyn Zhou Silver Creek High School, Baishakhi Ray Columbia University, Saikat Chakraborty Microsoft Research
Pre-print
14:52
15m
Talk
Syntax and Domain Aware Model for Unsupervised Program Translation
Technical Track
Fang Liu Beihang University, Jia Li Peking University, Li Zhang Beihang University
Pre-print