(Sigh... I realized I have no good way to mark your assignments if we go with Z3 , as I don't have remote access to a high performance Windows box. So, this is probably the last year we're still stuck using CVC3. CVC3 was an amazing solver in its day, and it's still great in a lot of different ways: open source, supports almost all theories, etc. But it's performance is no longer competitive. I spent some time investigating CVC4 and OpenSMT , which are newer, faster, and also open source, but they don't support enough theories yet. Z3 is actually available in a Linux version, but that version is stripped-down for competition and doesn't give satisfying assignments. The full version is free for non-commercial use, but runs only under Windows, and there isn't enough Windows compute power generally available as a departmental resource. So, CVC3 for one more year... If you do a project using an SMT solver, though, you should definitely look at using a faster solver. You can always go to the SMT Competition website to see lists of solvers, the logics they support, and how they did in competition.)
Please email me your sorting program (in any convenient procedural language, or pseudo-code), your program for generating the CVC3 scripts (preferably in C, C++, Perl, etc. -- basically, anything that will run easily under Linux), your generated CVC3 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 CVC3 . This is a completely free, open-source SMT solver, written by some of the very well-established people in the SMT community. On the positive side, it provides a lot of features that look like a programming language, supports a wide variety of theories, and is still widely used. On the negative side, it's now one of the slowest solvers that are still used. If you plan to do a project involving SMT solving, you'll want to use one of the newer systems instead of CVC3.
You can download
pre-built binaries (for Linux and Windows, too), from the
CVC3 download page.
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
This will only run on departmental Linux machines. See
for a list of servers available to you.
There's pretty good
, in particular, the
is a must-read.
Before you start the assignment itself, you'll probably want to
play with the solver a bit. Be sure to use the
option when you run interactively:
You can do things like ask whether 1 plus 1 equals 2:
QUERY (1 + 1 = 2);
a, b, c: INT;
ASSERT (a < b);
ASSERT (b < c);
QUERY (a < c);
QUERY (c <= a);
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 CVC3 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 CVC3, before you start writing your code.
That's it! I hope this is fun!
By the way, I have always 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.