**This workshop skips Thursday, July 4 (UC holiday), and concludes Friday, July 5.**

All talks are listed in Pacific Time. Schedule subject to change.

–
Coffee and Check-In
–
Opening Remarks
–
Linear Temporal Logic: From Infinite to Finite Horizon
Moshe Vardi (Rice University)
–
Synthesis of Privacy-Preserving Systems
Orna Kupferman (Hebrew University)
–
Panel: Reactive Synthesis - Open Questions and Challenges (Bernd Finkbeiner, Orna Kupferman, and Moshe Vardi)
–
Break
–
Synthesis from Hyperproperties
Bernd Finkbeiner (CISPA)
–
Program Repair for Hyperproperties
Borzoo Bonakdarpour (Michigan State University)
–
Lunch (on your own)
–
Specification-guided Reinforcement learning
Rajeev Alur (University of Pennsylvania)
–
Synthesis and Verification of Finite Horizon Tasks
Suguman Bansal (Georgia Institute of Technology)
–
Reception
–
Coffee and Check-In
–
A tutorial on on neurosymbolic techniques
Armando Solar-Lezama (MIT)
–
Learning From Contrastive Examples
Sandra Zilles (University of Regina)
–
Understanding the expressive power of transformers through the lens of formal language theory
Anthony Lin (TU Kaiserslautern)
–
Lunch (on your own)
–
Lifting as an abstraction
Necmiye Ozay (University of Michigan)
–
Grisette: Symbolic Compilation as a Functional Programming Library
Ras Bodik (Google DeepMind)
–
Coffee and Check-In
–
Automated Functional Synthesis: An Ideal Meeting Ground for Symbolic Reasoning and Machine Learning
Kuldeep Meel (University of Toronto)
–
Tractable Representations for Boolean Functional Synthesis
S. Akshay (Indian Institute of Technology Bombay)
–
Circuit Minimization with QBF and SAT-Based Exact Synthesis
Stefan Szeider (TU Wien)
–
Break
–
Discussion Groups
–
Lunch (on your own)
–
Proving Unrealizability (aka Verifying Infinitely Many Programs at Once)
Loris D'Antoni (University of Wisconsin - Madison)
–
Counterexample-Guided Inference of Modular Specifications
Bill Hallahan (Binghamton University)
–
Coffee and Check-In
–
On partial-order and automata techniques for analyzing communication
Anca Muscholl (University of Bordeaux)
–
Distributed Controller Synthesis for Deadlock Avoidance
Igor Walukiewicz (University of Bordeaux)
–
Synthesizing distributed protocols from global session types
Elaine Li (New York University)
–
Break
–
Synthesis from Knowledge Based Programs
Ron van der Meyden (University of New South Wales)
–
Ramsey Quantifiers in First-Order Logic: Complexity and Applications to Verification
Pascal Bergsträßer (University of Kaiserslautern-Landau)
Box Lunches and Afternoon Discussion Groups / Hike