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

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Despite its attractiveness and major research progress in the past decades, reactive synthesis is still in early-stage and has not gained popularity outside academia. We conducted an exploratory case study in which we followed students in a semester-long university workshop class on their end-to-end use of a reactive synthesizer, from writing the specifications to executing the synthesized controllers. The data we collected includes more than 500 versions of more than 80 specifications, as well as more than 2500 Slack messages, all written by the class participants. Our grounded theory analysis reveals that the use of reactive synthesis has clear benefits for certain tasks and that adequate specification language constructs assist in the specification writing process. However, inherent issues such as unrealizabilty, non-well-separation, the gap of knowledge between the users and the synthesizer, and considerable running times prevent reactive synthesis from fulfilling its promise. Based on our analysis, we propose action items in the directions of language and specification quality, tools for analysis and execution, and process and methodology, all towards making reactive synthesis more applicable for software engineers.

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