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.