Synthesis from within: extending SMT solvers with automated synthesis capabilities.
Prof. Cesare Tinelli ( University of Iowa )
- 14:00 2nd March 2022 ( week 7, Trinity Term 2022 )Via Teams
Recent research in automated software synthesis from specifications or observations has leveraged the power of SMT solvers to explore the space of synthesis conjectures efficiently. In most of this work, synthesis techniques are built around a backend SMT solver used as a black-box reasoning engine. In this talk, I will summarize the main outcomes of a successful multiyear research effort that instead incorporates synthesis capabilities directly within the SMT solver cvc5. I will describe some of the main techniques implemented in cvc5's synthesis module and then discuss the advances in performance and scope made possible by this approach.
Speaker bio
Cesare Tinelli is a F. Wendell Miller Professor of Computer Science at the University of Iowa. His main research interests include automated reasoning and formal methods. Professor Tinelli has done influential work in Satisfiability Modulo Theories (SMT), a field he helped establish through his research and service activities. He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He has co-led the development of the widely used and award-winning CVC3 and CVC4 SMT solvers, and currently co-leads the development of their successor cvc5. He received an NSF CAREER award in 2003, an HVC award in 2010, and a CAV Award in 2021. He is an associate editor of the Journal of Automated Reasoning and a founder the SMT workshop series. He has served in the steering committee of CADE, ETAPS, FTP, FroCoS, IJCAR, and SMT. He was the PC chair of FroCoS'11 and a PC co-chair of TACAS'15.Share this:
