An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

View on GitHub

Downloads

Documentation

Blog

Join the Conversation

People

Publications

Awards

Third Party Applications

Acknowledgements

Newsletter

Updates are posted every other month, sometimes more frequently.

by Yoni Zohar, 15 Feb 2024

Introduction The theory of sequences in cvc5 is relatively new. In essence, it is meant to model data structures such as List in Java, or std::vector in c++. Unlike the theory of arrays (which is actually a theory of maps), the theory of sequences is very rich, and allows, in addition to array-like read and write operations, to also use operators such as concatenation, sub-list, length, and more. Read More

by Alex Ozdemir, 26 Jan 2024

cvc5 is an SMT solver with support for many theories: integers, reals, bit-vectors, algebraic datatypes, separation logic, sets, bags, and more. This means that is can find satisfying solutions for formulas involving these kinds of objects. In this post, I explain the process of adding a new theory to cvc5: the theory of prime-order finite fields. Read More

by Amalee Wilson, 15 Dec 2023

Partitioning is a divide-and-conquer approach where a difficult problem is split into hopefully easier subproblems that can be solved in parallel. This strategy is notoriously difficult to get right with SMT problems. We found that while itâ€™s no panacea, partitioning can be used to diversify solving and reliably improve performance in a portfolio. Read More