Speaker
Cesare Tinelli
Abstract
Solvers for Satisfiability Modulo Theories (SMT) have become crucial components in safety- or mission-critical formal methods applications, in particular model checking, verification, and security analysis. Since state-of-the-art SMT solvers are large and complex systems, they are prohibitively difficult to prove correct. Hence, proof production is essential as a way to demonstrate instead the correctness of their responses, making those responses amenable to independent verification. Historically, the main challenges for proof production in SMT have been solver performance and proof coverage, often leading to the disabling of many sophisticated solving techniques when running in proof-production mode, or to coarse-grained, and harder to check, proofs.
The first part of this talk presents a flexible proof-production architecture designed to handle the complexity of versatile, industrial-strength SMT solvers, and discusses how it has been leveraged to produce detailed proofs, even for sophisticated reasoning components. The architecture, implemented in the state-of-the-art SMT solver cvc5, allows proofs to be produced modularly, as needed, and with various safeguards for correctness. The architecture supports the generation of textual proof certificates in different formats, for offline proof checking by external tools, as well as a rich API, which is useful for online integration of the SMT solver into other reasoning tools such as, for instance, skeptical proof assistants. Extensive experimental evaluations with both SMT-LIB benchmarks and benchmarks provided by industrial partners have shown that the new architecture results in greater proof coverage than previous approaches, imposes a small runtime overhead, and supports fine-grained proofs in the great majority of cases.
The second part of the talk gives an overview of a new generic language for expressing SMT proof certificates that builds on almost two decades of work and experience in proof generation and checking in SMT and combines the benefits of several previous efforts on the topic. While developed to express cvc5’s proof certificates, the language is meant to be useful to other SMT solvers as well. It is in fact a logical framework that can be customized with the specific proof system used by a solver through the definition of new symbols, binders and proof rules. In addition, it features an intuitive syntax for representing natural-deduction-style proofs and the ability to integrate other proof formats via the use of oracles. The talk briefly discusses an initial evaluation of the proof language, obtained with a companion checker for it and an instantiation to cvc5’s proof system. The evaluation shows the viability of high-performance, fine-grained proof production and checking for SMT.
Bio
Cesare Tinelli received a PhD in Computer Science from the University of Illinois at Urbana-Champaign in 1999 and is currently a F. Wendell Miller Professor of Computer Science at the University of Iowa. His research interests include automated reasoning, formal methods, software verification, foundations of programming languages, and applications of logic in computer science. Professor Tinelli has done influential work in automated reasoning, in particular in Satisfiability Modulo Theories (SMT), a field he helped establish through his research and service activities. His research has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, NSF, and ONR) and corporations (AWS, Facebook, GE, Intel, Rockwell Collins, and United Technologies) and his work has appeared in more than 130 refereed publications. He has co-led the development of the widely used and award-winning CVC3 and CVC4 SMT solvers, and co-leads the development of their successor CVC5. He is a founder and coordinator of the SMT-LIB initiative, a successful international effort for the standardization of benchmarks and I/O formats for SMT solvers. He has also co-led the development of StarExec, a cross community web-based service for the comparative evaluation of logic solvers, and leads the development of Kind 2 model checker. He received an NSF CAREER award in 2003; a Haifa Verification Conference award in 2010 for his role in building and promoting the SMT community; and a CAV Award in 2021 for his pioneering contributions to the foundations of the theory and practice of SMT. He is an associate editor of the Journal of Automated Reasoning and a founder of the SMT workshop series and the Midwest Verification Day series. He was the PC chair of FroCoS'11 and a PC co-chair of TACAS'15 and CADE-29.