Project Suggestions for SAV 2008
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
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.
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:
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.
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)
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.
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
Here is a list of SAV'07 Projects (note that the course last year covered different material).