Automated Synthesis: Fusing Formal Methods and AI
We increasingly entrust large parts of our daily lives to computer systems, which are becoming more complex. Developing scalable and trustworthy techniques for designing, developing, and verifying these systems is crucial. In this talk, we will focus on automated synthesis, a technique that uses formal specifications to automatically generate systems (such as functions, programs, or circuits) that provably satisfy the specified requirements. The talk will overview recent approaches that combine advances in automated reasoning, knowledge compilation, and machine learning to address a wide variety of practical automated synthesis problems. Additionally, we will introduce a state-of-the-art functional synthesis algorithm that leverages artificial intelligence to provide an initial guess for the system, followed by formal methods to repair and verify this guess, ensuring the system is correct by construction.