Blog

Updates are posted every other month, sometimes more frequently.

Induction and Conjecture Generation in cvc5

by Kartik Sabharwal, 17 Oct 2024

This post is intended for users of SMT solvers who are interested in the automation of proofs by induction. We demonstrate cvc5’s native support for structural induction over datatypes and its ability to synthesize lemmas that assist with such proofs, as described by Reynolds and Kuncak in Induction for SMT Solvers Read More

Interfaces for Understanding cvc5

by Andrew Reynolds, 15 Apr 2024

This blog post focuses on new interfaces for understanding the behavior of cvc5 and what to do when things go right and more importantly when they go wrong. We review the numerous diagnotic features of cvc5 and give tips on what to do when you are stuck. Read More

Reconstructing cvc5 proofs in Isabelle/HOL- Part I: Communication between Isabelle and cvc5

by Hanna Lachnitt, 15 Mar 2024

If you have used the cvc5 SMT solver before you know that it can solve many complicated problems fast, especially for the theories it supports! But can other programs profit from cvc5’s efficiency too? And if so, how can cvc5 effectively communicate with these external tools? Could we use their feedback to increase our trust in cvc5’s result even more? Read More

A Theory of Sequences in cvc5

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

Adding a New Theory to cvc5

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

Partitioning Strategies for Distributed SMT Solving

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