This list of projects is very preliminary. Your own ideas are welcome. This list is periodically updated.

Implement a general verification condition generator that handles data structures and accepts programs in a subset of a working programming language. Either write a parser or connect it to an existing compiler infrastructure (for example: Scala compiler, Java bytecode reader, CIL system).

You may choose a particular language subset such as:

• purely functional programs that manipulate algebraic data types
• programs that manipulates sets and relations, as the SETL programming language

Explore techniques for solving constraints over finite domains given by expressive constructs such as recursive definitions and transitive closure.

The theoretical foundation is based on the fact that, if we fix a finite domain, then we can express a wide range of constraints over such domains, which are given by user-specified functions in a subset of a purely functional programming language. For example, quantification becomes an iteration or list fold, transitivity becomes computation of the set of reachable nodes in a graph. The solver for such finite constraints combines search for interpretation of relations with checking whether given constraint is true in interpretation constructed so far.

Relevant techniques are finite model finding, especially Alloy and Kodkod, as well as TestEra and Korat, but deployed in the context of purely functional programs.

An input to such a tool would be a pure function taking as input an interpretation and returning 'true' iff the given constraint is true in the given interpretation. The tool would search for an interpretation for which the given function becomes true. Among important subproblems is a generalization of the notion of boolean constraint propagation to such more general domains.

Write an interactive theorem prover in Scala or Ocaml, following the widely-used LCF approach:

• A Metalanguage for interactive proof in LCF
• Slides by John Harrison

The interactive prover should allow Scala programmer to write proofs in the form of Scala programs. Explore the suitability of Scala as a domain-specific language for writing proofs.

Modelling distributed systems using combinators and verifying them using model checking or proof-based methods.

Design an algorithm for infering an interesting class of loop invariants.

Build a simple SMT (satisfiability modulo theory) solver that uses e.g. Nelson-Oppen combination.

Write a quantifier elimination procedure for a theory such as term algebras, or implement a version of Omega test and use it to analyze properties of programs manipulating arrays and integers.

• Omega test (and related papers)

Investigate techniques for constructing representations of infinite models for first-order formulas.

Explore techniques for proving inductive statements such as

• Test set induction, or from Citeseer

and their application to software verification.

Design a language where complex data structures are easy to prove correct. Possibly use ideas from separation logic.

Improve your SAT solver further or experiment with new ideas. Your goal would be to get a working solver at least as good as the best solver we had in class competition.

Enable simultaneous use of theorem proving and test-case generation techniques for some subset of the speficiation language.

Accepting TPTP syntax and handling equality, but not necessarily implementing sophisticated orderings.

Use Jahob system to verify some more data structures like these.

Here is a list of SAV'07 Projects (note that the course last year covered different material).