• 1st Call for Papers:
    January 10, 2022

    Paper Submission (extended!):
    May 10, 2022 AoE
    May 15, 2022 AoE

    Author Notification:
    May 31, 2022

    August 11, 2022



<SYNT 2022>
9:00 - 9:02 Welcome!
Session 1
Session Chair: TBD   
09:02-10:00 Invited Talk: Inductive and Parameter Synthesis to Find POMDP Controllers
Joost Pieter Katoen, RWTH, Aachen

Partially observable Markov decision processes (POMDPs) are a central model in planning under uncertainty in AI. POMDPs are probabilistic models with non-determinism, and -- most importantly -- its states are partially observable. The fact that one cannot determine the current state complicates finding POMDP controllers, i.e., policies that resolve the non-determinism based on the observation history so far. Example objectives are indefinite-horizon reachability and expected reward properties. A range of efficient controller synthesis techniques exist in the AI community. In this talk, I will present approaches from formal verification and synthesis inspired by on the one hand, parameter synthesis on Markov chains, and on the other hand, CEGIS for sketching of probabilistic programs. I will explain the ins and outs of these approaches and show that they provide a competitive alternative to techniques from AI planning.

10:00-10:15 Towards Synthesis in Superposition
Petra Hozzová, Laura Kovács and Andrei Voronkov


10:15-10:30 LTL Synthesis with Transformer Neural Networks
Frederik Schmitt, Christopher Hahn, Markus N. Rabe and Bernd Finkbeiner.


10:30-11:00 Break
Session 2
Session Chair: TBD   
11:00-12:00 Invited talk: Beyond Counterexamples: Satisfiability and Synthesis Modulo Oracles
Elizabeth Polgreen, University of Edinburgh

In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification) phase. Many (most) synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) solvers to provide counterexamples. But what if a white-box oracle is either not available or not easy to work with? In this talk, I will present a framework for solving a general class of oracle-guided synthesis problems which we term synthesis modulo oracles (SyMO). In this setting, oracles are black boxes with a query-response interface defined by the synthesis problem. This allows us to lift synthesis to domains where using an SMT solver as a verifier is not practical. I will formalise what it means for a problem to be satisfiable modulo oracles, and present algorithms for solving Satisfiability Modulo Theories and Oracles (SMTO), and Synthesis Modulo Oracles (SyMO). I will demonstrate some prototype case-studies for SyMO and SMTO, and show how the use of oracles allows us to lift solve problems beyond the abilities of classic SMT and synthesis solvers.

12:00-12:15 Complexity of Relational Query Synthesis
Aalok Thakkar, Rajeev Alur and Mayur Naik


12:15-12:30 Interactive Debugging of Concurrent Programs under Relaxed Memory Models
Aakanksha Verma, Pankaj Kumar Kalita, Awanish Pandey and Subhajit Roy


12:30 - 14:00 Lunch Break
Session 3
Session Chair: TBD  
14:00-14:20 Reactive Synthesis of LTL specifications with Rich Theories
Andoni Rodriguez and César Sánchez


14:20-14:40 Regex+: Synthesizing Regular Expressions from Positive Examples
Elizaveta Pertseva, Mark Barbone, Joey Rudek and Nadia Polikarpova


14:40-15:00 Inferring Environment Assumptions in Model Refinement
Srinivas Nedunuri and Douglas Smith


15:00 - 15:20 A Framework for Transforming Specifications in Reinforcement Learning
Rajeev Alur, Suguman Bansal, Osbert Bastani and Kishor Jothimurugan


15:20-15:30 SYNTCOMP results
Guillermo A. Pérez
15:30 - 16:00 Break
Session 4
Session Chair: TBD  
16:00-16:10 SyGuS-IF results
Andrew Reynolds
16:10 - 17:00 Future Work and Open Challenges Panel – Authors+Chairs
17:00 - 17:05 Closing
</SYNT 2022>