• you are not restricted to these ideas, but please discuss the suggestions with me first
• some of the projects below have been assigned already
• once you know which project you will like to do and you discussed it with me, email me with project title and names of people on the project
• these ideas are meant to be open-ended, so there is no such thing as “entirely finished project” and you can do only part of it. Overall, the pace of work on your project should be similar to the pace we had for homeworks (you will have more time for project, but the project is bigger than any single homework and closer to the sum of all homeworks)
• once you choose the project you should regularly discuss your progress with me, approximately once a week

Verify completeness and disjointness of guarded patterns in Scala.

• connect to some pass (to be determined where exactly)
• do analysis of completeness of pattern matching of guards (optionally disjointness if useful)
  • look at guards that have no loops or procedure calls
  • verification condition generation + some theorem prover
• can represent completeness as unreachability of the default case

• can we use formDecider.opt or some other tool that formDecider uses

• some issues: do we need procedure preconditions to check for completeness of interesting data structures?

do we need more expressive type systems/constraints to encode invariants on data structures

• check e.g. ocaml polymorphic variants and
• refinement types

Implement a bug finder based on SAT.

For example, you could start from formulas in Jahob and generate, in order of going more and more detailed:

• alloy formulas http://alloy.mit.edu
• code that invoked kodkod solver used within Alloy http://web.mit.edu/~emina/www/kodkod.html
• input to a SAT solver directly using the standard DIMACS format

For techniques you can see this thesis

http://theory.stanford.edu/~aiken/publications/theses/xie.pdf

and this paper:

http://sdg.csail.mit.edu/pubs/2006/dennis_modular.pdf

This can be a longer term thing, but even if you do a working translation from Jahob formulas into Alloy formulas it will be interesting and useful.

Implement a static analyzer for linear constraints on integer variables using domains such as octagons, intervals, or polyhedra.

Incorporate the analyzer into Jahob.

Develop techniques for extracting such constraints from general Jahob formulas.

Implement a typestate analyzer for Jahob following the ideas in

http://lara.epfl.ch/~kuncak/papers/LamETAL05GeneralizedTypestateCheckingDataStructureConsistency.html

Implement an efficient run-time checker or compiler for specifications.

Define a class of formulas that can be evaluated at run time.

• http://www.mit.edu/~kkz/ZeeRV07.pdf
• http://www.mit.edu/~kkz/rv07.pdf
• ftp://ftp.cs.iastate.edu/pub/techreports/TR03-09/TR.pdf
• http://fsl.cs.uiuc.edu/index.php/MOP:_An_Efficient_and_Generic_Runtime_Verification_Framework

Verify an interesting Java program, such as a data structure, using Jahob.

Theoretical project.

Try to come up with a quantifier elimination procedure for monadic second-order logic over strings.

Compare results to to Presburger arithmetic quantifier elimination.

Generalization to quantifier elimination for Monadic Second-Order Logic over Trees.

@InCollection{Thomas97LanguagesAutomataLogic,
  author =       {Wolfgang Thomas},
  title =        {Languages, Automata, and Logic},
  booktitle =    {Handbook of Formal Languages Vol.3: Beyond Words},
  publisher =    SPRINGER,
  year =         1997
}

Develop a set of proof rules that allow statements such as assume and assert statements to be used to prove arbitrary invariants in imperative programs.

For example, to prove

s1;
assert (ALL x. P(x))

it should be possible to declare

var x;
havoc x;
s1;
assert P(x);

when certain properties hold for s1.

To prove

assert (EX x. P(x))

we should be able to prove

assert P(t)

for some term t.

You need to generalize these ideas, prove that they work and explore what class of properties we can prove using them.

Generalize the this result on sets with cardinality bounds by bounding certain parameters incorporating relations. Evaluate the applicability of these polynomial algorithms to a constraints that are NP hard.

Create a summary (in form of wiki) of a substantial number of logics that are useful for software analysis and verification. State complexity of algorithms for these logics and general techniques used, and reference appropriate papers.

In the context of Jahob, explore translation from a subset of full-fledged language like Java into guarded command language, enabling verification of more real-world programs.

Develop a decision procedure for reasoning about trees with reachability predicate. The logic should be in NP.

• http://www.cs.ubc.ca/~zrakamar/publications/vmcai2007-rbh.pdf
• http://www.cs.ubc.ca/cgi-bin/tr/2005/TR-2005-19.pdf
• http://eeyore.cs.nyu.edu/~acsys/pubs/single-parent.pdf

Implement a translation from QFBAPA to SAT using the ideas from cade07paper.pdf.

Compare the results to an existing translator to SMT format.

Develop techniques for verifying programs written in an imperative language with transactional memory.