Program
| GMT+3 | ||
| <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 TBA |
|
| 10:15-10:30 |
LTL Synthesis with Transformer Neural Networks Frederik Schmitt, Christopher Hahn, Markus N. Rabe and Bernd Finkbeiner. TBD |
|
| 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 TBD |
|
| 12:15-12:30 |
Interactive Debugging of Concurrent Programs under Relaxed Memory Models Aakanksha Verma, Pankaj Kumar Kalita, Awanish Pandey and Subhajit Roy TBD |
|
| 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 TBD |
|
| 14:20-14:40 |
Regex+: Synthesizing Regular Expressions from Positive Examples Elizaveta Pertseva, Mark Barbone, Joey Rudek and Nadia Polikarpova TBD |
|
| 14:40-15:00 |
Inferring Environment Assumptions in Model Refinement Srinivas Nedunuri and Douglas Smith TBD |
|
| 15:00 - 15:20 |
A Framework for Transforming Specifications in Reinforcement Learning Rajeev Alur, Suguman Bansal, Osbert Bastani and Kishor Jothimurugan TBD |
|
| 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> | ||