**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)
Video
–
Synthesis of Privacy-Preserving Systems

Orna Kupferman (Hebrew University)
Video
–
Panel: Reactive Synthesis - Open Questions and Challenges (Bernd Finkbeiner, Orna Kupferman, and Moshe Vardi)
–
Break
–
Synthesis from Hyperproperties

Bernd Finkbeiner (CISPA)
Video
–
Program Repair for Hyperproperties

Borzoo Bonakdarpour (Michigan State University)
–
Lunch (on your own)
–
Specification-guided Reinforcement learning

Rajeev Alur (University of Pennsylvania)
Video
–
Synthesis and Verification of Finite Horizon Tasks

Suguman Bansal (Georgia Institute of Technology)
Video
–
Reception
–
Coffee and Check-In
–
A tutorial on on neurosymbolic techniques

Armando Solar-Lezama (MIT)
Video
–
Learning From Contrastive Examples

Sandra Zilles (University of Regina)
Video
–
Understanding the expressive power of transformers through the lens of formal language theory

Anthony Lin (TU Kaiserslautern)
Video
–
Lunch (on your own)
–
Lifting as an abstraction

Necmiye Ozay (University of Michigan)
Video
–
Grisette: Symbolic Compilation as a Functional Programming Library

Ras Bodik (Google DeepMind)
Video
–
Coffee and Check-In
–
Automated Functional Synthesis: An Ideal Meeting Ground for Symbolic Reasoning and Machine Learning

Kuldeep Meel (University of Toronto)
Video
–
Tractable Representations for Boolean Functional Synthesis

S. Akshay (Indian Institute of Technology Bombay)
Video
–
Circuit Minimization with QBF and SAT-Based Exact Synthesis

Stefan Szeider (TU Wien)
Video
–
Break
–
Discussion Groups
–
Lunch (on your own)
–
Proving Unrealizability (aka Verifying Infinitely Many Programs at Once)

Loris D'Antoni (University of Wisconsin - Madison)
Video
–
Counterexample-Guided Inference of Modular Specifications

Bill Hallahan (Binghamton University)
Video
–
Coffee and Check-In
–
On partial-order and automata techniques for analyzing communication

Anca Muscholl (University of Bordeaux)
Video
–
Distributed Controller Synthesis for Deadlock Avoidance

Igor Walukiewicz (University of Bordeaux)
Video
–
Synthesizing distributed protocols from global session types

Elaine Li (New York University)
Video
–
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)
Video
Box Lunches and Afternoon Discussion Groups / Hike