Professor Cesare Tinelli and long-time Stanford collaborator and Principal Investigator Clark Barrett were recently awarded a $1.5 million grant from the National Science Foundation for their project entitled POSE: Phase II: An Open-Source Ecosystem for the cvc5 SMT Solver.

Tinelli’s research focuses primarily on the reliability of computer systems that are becoming so crucial to modern society. Techniques that aim to construct more reliable computer systems rely on producing and proving verification conditions. Verification conditions are mathematical formulas that capture properties of the software, and research in automated reasoning is dedicated to proving these formulas automatically.

Modern automated reasoning tools can prove billions of verification conditions daily. One of the most successful models is called satisfiability modulo theories (SMT), and tools using this model are called SMT solvers. This aims to transform a highly specific SMT solver project called cvc5 from an academic project to an open-source ecosystem (OSE).

Collaborations with both Certora¹ and Amazon - namely their AWS entity - have also aided Tinelli’s research - and that of cvc5 team - by providing challenge problems from industrial applications. Certora shared constraints corresponding to verification of numeric intensive software used in Cryptocurrency toolchains, and Amazon has been able to contribute statistics and feedback for their use of cvc5 for security analysis in their Zelkova reasoner². In addition, per Andy Reynolds - UIowaCS Research Scientist - "Since correctness is highly important, Amazon has requested support for proofs in SMT solvers over a variety of theories. We have developed a new proof language called AletheLF [and a new proof checker]. There have been a number of other new applications that have a need for SMT solvers within Amazon as well, for instance for software verification and interactive theorem proving."

The NSF project’s goals include establishing and growing the SMT ecosystem, implementing structures to organize and govern, building a community of developers and users, and establishing a plan to sustain the tool and its ecosystem. The project will make SMT solvers more accessible to a broader audience by making cvc5 available on more platforms and developing tutorials to aid users in their understanding of the tool. The project will also expand its community by organizing workshops for both developers and users and establishing organization and governance procedures to welcome new members.

Tinelli’s project hopes to produce an international community of developers and users of cvc5 along with a sustainable plan for coordinating and governing members of the community and the adoption of industry best-practices for security and code quality in cvc5. By doing so, this project will serve the larger goal of improving the reliability of computer systems.

¹"Bit-Precise Reasoning via Int-Blasting" published at 23^rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022) "

² "A Billion SMT Queries a Day" blog post and 2022 CAV keynote talk by Neha Rungta, director of applied science with AWS, talk about this application.