![Satisfiability_hi-res-logo](/sites/default/files/styles/workshop_banner_sm_1x/public/2023-01/Satisfiability_hi-res.jpg?h=b86da943&itok=JIajwKvC)
Abstract
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.