Please email me your sorting program (in any convenient procedural language, or pseudo-code), your program for generating the CVC4 scripts (preferably in C, C++, Perl, Python, etc. -- basically, anything that will run easily on a CS Department Linux machine), your generated CVC4 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:

• Write a small, specific program, namely a program to sort a small, fixed number of integers. This is just to give you a concrete program to verify, so you may write your sorting program in any reasonable, procedural language, or even in pseudo-code. Given that it's hard to determine when to terminate a while-loop when doing symbolic execution, I'll encourage you to use a sorting algorithm where termination occurs after a fixed amount of work (e.g., mergesort, or selection sort, or a hardware sorting network, or even two nested loops from 0 to n-1 walking through the array and swapping out-of-order neighbors, but not something like standard bubblesort, where you terminate when there are no out-of-order pairs to swap). Start small! Try 4 first. Or maybe even 2 or 3. Then increase this number. (In the past, I don't think anyone successfully verified a program sorting more than 13 or so integers, but that was with older, less efficient SMT solvers. See how big you can go.)
• Once you know what your little sorting program is, your goal is to create the SMT problem instance to verify that your program sorts. Note that you are not required to verify that the output is actually a permutation of the input (which is hard to specify), but just that the output is sorted. Conceptually, you are doing the same thing you did in Assignment 2, except that instead of a circuit, you have a program, and your output is an SMT instance, rather than a SAT instance.
• To do the above, you will most likely want to write a program to generate the output for you! (Again, as in Assignment 2, where the program you (and I) wrote generates the SAT instance, which you then give to the SAT solver.) However, unlike Assignment 2, you are NOT required to have your program parse and analyze your sorting program. Instead, you can use any kludgey hacky way of programming you'd like to generate the specific SMT instance for your specific sorting program. You can write this program in any language that you like (e.g., C, C++, Perl, Python, etc.), as long as it runs easily on the CS Department Linux machines. (Note that it might be easier to write a simple parser to generate the CVC4 scripts, though. Some students have chosen to do so in the past. I leave that up to you.)
• Of course, you'll want to try out your output on a real SMT solver.

The SMT solver we'll use for this assignment is called CVC4 . This is a completely free, open-source SMT solver, written by some of the top people in the SMT community. CVC4 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 is much faster, and is now competitive with the best solvers available. (However, if you do a project using an SMT solver, you might also consider trying Z3 , which is generally 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.) (New in 2021: There's now a CVC5, but it doesn't look as well-supported yet, and given my personal circumstances, let's go with CVC4 again this year. But you might look into using CVC5 in your projects.)

You can download pre-built binaries (for Linux and Windows, too), from the CVC4 downloads 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 at /isd/users/software/cvc4-1.8-x86_64-linux-opt This will only run on CS departmental Linux machines. See this link for a list of servers available to you. (Or use your own machines, or from your research labs...)

There's pretty good on-line documentation at the CVC4 homepage. You'll likely want to get started at the "Getting Started" link. CVC4 has multiple input languages, but I generally use its native input language, which is documented here. Before you start the assignment itself, you'll probably want to play with the solver a bit. You'll want to use the -im options to put the solver in incremental mode as well as allow it to generate counter-examples (models):
/isd/users/software/cvc4-1.8-x86_64-linux-opt -im
(By the way, for those of you new to Unix/Linux, ask or read up about symbolic links. You'll probably want to create a link to the CVC4 solver, so you don't have to keep typing the full pathname.) You can do things like ask whether 1 plus 1 equals 2:
QUERY (1 + 1 = 2);
or try:
a, b, c: INT;
ASSERT (a < b);
ASSERT (b < c);
QUERY (a < c);
QUERY (c <= a);
COUNTERMODEL;


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 CVC4 script that would be appropriate for that example. (Note that CVC4 wants input files to have the extension .cvc if the input language is the CVC native language.) You'll probably want to play with this example a bit, to get used to the syntax, and CVC4, 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.