Feedback on Proof Failure

title:Feedback on Proof Failure
keywords:Static Verification, Runtime Checking, Test Generation
topics:Languages, Logics and semantics
contact:W.H.M. Oortwijn MSc & prof.dr. M. Huisman
to be started:any time


Description

Program logics can be used to reason about the functional correctness of software. For example, the Java Modelling Language (JML) can be used to describe the functional behaviour of Java programs and tools for static checking may be used to verify whether the program behaves as specified. However, deductively proving program correctness may be very subtle: if the specification is slightly wrong or if some edge cases are missing, the verifier may time-out or might produce a (large) number of (verbose) errors.


Petiot et al. [1] proposes a technique to help the user to identify the reason for a proof failure, implemented in Frama-C, a verifier for C program. The proposed technique transforms the annotated C program to be able to generate tests and uses automated testing to find a counter-example to the annotations. This technique is suitable for finding sub-contract weaknesses and the counter-examples may help the user to diagnose the proof failure.


This project is about integrating a similar technique in the OpenJML tool set. The goal of this project is to identify sub-contract weaknesses of JML annotations and to construct counter-examples to help the user to better understand the problems. For this project you should extend the OpenJML tool set to support these features and you should demonstrate your extensions on a number of verification examples.

References

  1. Your Proof Fails? Testing Helps to Find the Reason (Digital version available here)