Project Suggestions for SAV 2008

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

Verification-Condition Generator

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

Solving Computable Constraints over Finite Domains

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.

Interactive Prover

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

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.

Verifying Composable Distributed Systems

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

Invariant Inference

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

SMT Solver

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

Quantifier Elimination

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.

Infinite Model Construction

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

Theorem Proving with Induction

Explore techniques for proving inductive statements such as

and their application to software verification.

Language Design for Verifiability

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

SAT Solver

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.

Combine Specification-Based Testing with Static Analysis

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

Simple Resolution-Based Prover

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

Verification Case Study

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

Other Examples

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