Reactive Synthesis Empowered by Logical Reasoning
7Rayna Dimitrova (CISPA Helmholtz Center for Information Security)
https://simons.berkeley.edu/talks/rayna-dimitrova-cispa-helmholtz-center-information-security-2023-04-20
Satisfiability: Theory, Practice, and Beyond
The advances in Boolean satisfiability (SAT) have made possible the successful SAT-based techniques in formal verification, and, more recently, in reactive synthesis. The task of synthesis is to construct an implementation of a system automatically from a formal specification. Reactive synthesis is a highly attractive and increasingly viable alternative to manual system design, with applications such as the design of communication protocols and control of autonomous systems. Many of these applications necessitate a shift from classical synthesis techniques toward methods that require logical reasoning beyond SAT (e.g., partial weighted MaxSAT or maximum model counting). In this talk, I will give an overview of SAT-based verification and synthesis, recent developments, and the challenges they present for logical reasoning beyond SAT.