Department of Computer Science
CPSC 513: Playing with an SMT Solver


Please email me your sorting program (in any convenient procedural language, or pseudo-code), your program for generating the SMT-LIBv2 scripts (preferably in C, C++, Perl, Python, etc. -- basically, anything that will run easily on a CS Department Linux machine), your generated SMT-LIBv2 scripts, and a brief description of what you thought of the assignment. (BTW, please send this to me as plain ASCII text. Not as a PDF, not as a Word file, etc. And please don't email me the binaries.)

OK, so what is the assignment? The goal of this assignment is to give you an understanding of how to write a symbolic execution engine to verify software with an SMT solver, but to save you (and me) the pain of writing a symbolic execution engine. Instead, you will:

The SMT solver we'll use for this assignment is called CVC5 . This is a completely free, open-source SMT solver, written by some of the top people in the SMT community. CVC5 traces its history back to the solvers that launched the recent interest and success of SMT solvers, but for a long time, the earlier solvers (CVC, CVC-Lite, CVC3) had a reputation for being flexible, but slow. CVC4 caught up with the fastest solvers, and now CVC5 is among with the best solvers available. (However, if you do a project using an SMT solver, you might also consider trying Z3 , which has long been considered the fastest SMT solver. Z3 used to have licensing issues (free for non-commercial use only, and only supporting Windows), which is why I had standardized on CVC, but Z3 is now under the MIT license and more generally available. You can always go to the SMT Competition website to see lists of solvers, the logics they support, and how they did in competition.)

You can download pre-built binaries (for Linux, MacOS, and Windows), from the CVC5 downloads page. (Note that on my very old home and office machines, I had to use the pre-built binary for version 1.1.2 instead of the newest 1.2.0, which apparently uses some AVX2 or newer instruction set extensions that my old machines don't support.) You can also download source and build your own copy, if you'd like. I have a 64-bit Linux version on the departmental machines at /isd/users/software/cvc5

There's pretty good on-line documentation for CVC5. You'll likely want to get started using the QuickStart Guide. The input language for CVC5 (and Z3, and pretty much all SMT solvers now) is called SMT-LIB v2. The language is designed to be powerful and flexible, and therefore feels hard to learn and use (to me). Here is the official documentation for the language but it might be easier to just look at examples in the CVC5 documentation.

Here's an example in pseudo-C that sorts three integers. . (You may want to use an array for more data entries, instead of separately named variables as I did here.) And here's an example of a SMT-LIBv2 script that would be appropriate for that example. You'll probably want to play with this example a bit, to get used to the syntax, and CVC5, before you start writing your code.

That's it! I hope this is fun!


By the way, I had originally intended to make this assignment just like Assignment 2, where you (or actually, I) would write a symbolic execution engine for a simple programming language, and this would generate queries to the SMT solver. Then, I would give you a sorting program written in that simple programming language, and you'd use the symbolic execution engine to generate SMT queries, and solve them with the SMT solver. However, this would require me to make up a simple programming language and write up a parser and interpreter for it, and I keep running out of time. Fortunately, each time I have used this assignment, student feedback has actually been quite positive. Furthermore, using scripts to generate inputs to other programs is actually a common and useful way to tackle problems, so it's fun to give that a go, too. I'll appreciate your feedback on whether you think I should make the time to do the assignment more like Assignment 2 in future years.