SAS 2022
Mon 5 - Wed 7 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Tue 6 Dec 2022 16:30 - 17:00 at AMRF Auditorium - Invariant and Program Synthesis Chair(s): Subhajit Roy

Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodríguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. We further present a novel technique that automatically synthesises polynomials, in the defective variables, that admit closed-form solutions and thus lead to polynomial loop invariants. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

Tue 6 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
Invariant and Program SynthesisSAS at AMRF Auditorium
Chair(s): Subhajit Roy IIT Kanpur
15:30
30m
Talk
Bootstrapping Library-Based Synthesis
SAS
Kangjing Huang Purdue University, USA, Xiaokang Qiu Purdue University, USA
16:00
30m
Talk
Automated Synthesis of Asynchronizations
SAS
Sidi Mohamed Beillahi University of Toronto, Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea Ecole Polytechnique / LIX / CNRS, Shuvendu Lahiri Microsoft Research
16:30
30m
Talk
Solving Invariant Generation for Unsolvable Loops
SAS
Daneshvar Amrollahi Stanford University, Ezio Bartocci TU Wien, George Kenison TU Wien, Laura Kovács TU Wien, Marcel Moosbrugger TU Wien, Miroslav Stankovič TU Wien