Sound Loop Verification in ESC/Java3
Note: Some intitial work was accomplished on this project by PhD student Mikoláš Janota. Please contact him for details.
- Supervisor Dr. Joseph Kiniry
- Subject Area Software Engineering with Applied Theoretical Computer Science
- Pre-requisites Strong knowledge of Java and reasonably strong mathematical background
- Co-requisites (things you must learn along the way) Programming language semantics, formal specification, extended static checking, logic
- Subject Coverage Semantics, Extended Static Checking
- Project Type Design and Implementation
- Hardware/Software PC, laptop or workstation capable of running Java and Eclipse
Description
When ESC/Java was originally written, the developers never intended to attempt to fully specify and verify the correctness of program loops. Thus, the specification language supported making assertions about loop invariants (to prove safety), but not loop variants (to prove termination).
Because of these design and specification limitations, ESC/Java only reasons about the partial correctness of loops, effectively by unrolling them a few times and verifying that the unrolled loop fulfills the invariant. This technique is neither sound nor complete and is a known deficiency of ESC/Java.
Later, additions were made to attempt to realised total correctness verification techniques (e.g., using the -loopSafe switch). While this technique works in practise, it depends upon the user writing loop invariants and variants in a very precise fashion.
ESC/Java2 supports the full JML language which includes loop invariants, loop variants, and more. Additionally, we now are beginning to support new provers that look more capable than the original prover, Simplify. Thus, it is an opportune time to improve support for loop verification to ESC/Java3.
The goal of this project is to design and implement a new subsystem in ESC/Java3 that will automatically (a) characterise which loop verification methodology is appropriate for a given check, (b) perform the sound and complete verification of fully specified loops, and (c) incorporate recently proposed techniques in abstract interpretation to automatically derive loop invariants and variants.
Mandatory Goals
- Become familiar with the ESC/Java2 calculi and their soundness and completeness issues.
- Become familiar with the techniques used to specify and reason about the partial and total correctness of loops.
- Design and implement a sound and complete loop verification algorithm for ESC/Java3.
Discretionary Goals
- Coauthor, submit, and publish a paper on this work.