If you're interested in either of these projects, and have the relevant background, drop me an email at razvan at comp dot nus dot edu dot sg

Extend JML with modal logic/separation logic -- formalization in Coq

The Java Modeling Language is a specification language for Java programs, using Hoare style pre- and post-conditions and invariants, which has been implemented in verification tools such as ESC/Java and Krakatoa. One of the main pitfalls of the Hoare formalism, and consequently of JML, is its inability to produce concise reusable proofs for a programming language with concurrency, mutable store, dynamic allocation, and garbage collection. Nevertheless, in recent developments, separation logic and dynamic logic have been jointly used, quite successfully, to correct this drawback.

The purpose of this project is to extend the JML specification language with separation and modal constructs that would make it more expressive, and thus more concise in expressing mutable store properties such as pointer (un)aliasing, or the fact that a possible concurrent invocation of the garbage collector will leave the current instruction unaffected. The new specification language features must be accompanied by appropriate inference rules, which are expected to produce concise reusable proofs for programs that manipulate arrays, linked lists, trees, and graphs. The entire approach must be formalized in a proof assistant (preferrably Coq), and proven sound mechanically.

Interactive verification of object-oriented programs

This project is a possible concurrent development of the one listed above. Following the example of the Krakatoa program verifier, which can be used to interactively develop correctness proofs for JML annotated Java programs, we propose to build an interactive program verifier for the extension of JML proposed above.

Automation of inductive proofs in Coq

Proofs by induction are notoriously hard to automate. The main  difficulty is that in general the number of choices for every proof step is large, and that results in a search space of prohibitive size. However, in recent work, we have successfully applied search techniques to "discover" induction proofs for implication-based goals in a constraint logic programming setting. Our search techniques employ a notion of interpolation which, in a constraint-based setting, happens to have a variety of instances that can be efficiently implemented.

The aim of this project is to implement our method in a more general setting, as a tactic in the proof assistant Coq. The challenge here is that, in the realm of recursively defined predicates that Coq
allows, the notion of interpolation is no longer as straightforward as in the constraint based setting, and requires an innovative implementation.

An extensible tactical language for proof algorithms
 

This is a possible concurrent project with the one listed above. For many proof assistants, the tactical language (i.e. the language used to develop new tactics) is not powerful enough to allow the development of search techniques such as the one mentioned above. In this project, we would aim to extend the tactical language of a proof assistant (preferrably Coq) in such a way that the search algorithm could be implemented in this language.

Extraction of efficient programs from verification proofs

Coq is a theorem prover based on the Curry-Howard isomorphism. This isomorphism specifies that the type of an expression in a typed higher-order programming language (such as Caml) can be interpreted as a logic formula. The arrow that denotes a function type could be interpreted as implication, while the tupling constructor could be interpreted as conjunction. Based on the Curry-Howard isomorphism, a logic formula is true only when there exists an expression having a type that is syntactically identical with the formula of interest. For instance, the formula A->A (that is, A implies A) is true because for any type A we can construct an expression with type A->A (i.e. function from A to A). This expression is (fun x:A=>x), that is, the identity function. In the Coq proof assistant, as the user develops a proof by successively applying tactics to the goal at hand, the system builds in the background an expression of a type syntactically identical to the goal. This expression can be translated into a programming language and executed, performing an operation that guarantees that the postcondition is valid. For instance, in proving that a list is sorted, a by-product would be a sorting function, that is, a function whose output is guraranteed to be sorted. This function can be translated into Ocaml, and used to perform sorting operations on lists. This operation is called _extraction_ . However, since the proof assistant's main objective is to produce a concise, readable proof, the extraction is, in general, not a very efficient function. In fact, it is completely counterintuitive for the user, as he/she develops the proof, to produce efficient code.

In this project, we would like to explore a methodology that would allow the user to control the efficiency of their extraction in a step-by-step manner. This can be done by assigning a semantics to each tactic, and representing the proof in a way that makes its time complexity apparent. Armed with a correct set of tactics, the user could, throughout an interactive proof, not only produce an extraction that proves the goal of interest, but also produce an extraction that is efficient.