Toward a cooperative and open framework for the development of certifiable software

I participated last week in the VerifyThis Verification Competition, which took place on Thursday afternoon during the Formal Methods 2012 conference in Paris. The goal was to apply verification tools to three small challenge programs, to compare approaches and learn from each other’s tools.

I used Ada 2012 as a programming and specification language (using preconditions and postconditions to specify contracts for subprograms) and our prototype GNATprove, a proof tool developed in project Hi-Lite, to formal verify that the code implements its contract and does not raise run-time errors (integer overflows, array index out of bounds, etc.) I completed challenge 1 and I did a part of challenge 2, but I had not enough time to complete it or start on challenge 3.

The competition was followed on Friday by a very interesting explanation session where each team showed how it addressed the problems with its tools. It was particularly interesting to see different solutions from teams using the same language (for example, the two teams using Why3 had quite different solutions for challenge 2), as well as the interaction between the user and the proof tool in KIV, KeY, Why3, etc. I think the problems and their solutions will be added soon to the VerifyThis repository, but if you cannot wait, you can also ask the organizers for a tarball of the submissions.

To come to the title of this post, the organizers awarded a distinction to GNATprove for its integration of proving and run-time assertion checking, of which I’m very proud. As I explained them, this integration was essential in helping me during the competition:

• For the first problem, I was stuck with a postcondition that I could not prove, and I did not manage to figure out why. So I decided to write a small test to make sure at least that the code and the contract were not contradictory. I executed it, and it raised an exception saying the postcondition was wrong! (because Ada 2012 contracts are executable, the compiler can transform them into run-time assertions, including quantifiers that are transformed in loops) It was then easy to pinpoint the root cause of the problem, the use of “<" instead of "<=" in the test of the main loop.
• For the second problem, I decided to implement the iterative version of the algorithm, which is more complex to specifiy and verify than the recursive one, but also more representative of critical embedded software. The algorithm is divided in two passes, each one performing two nested loops on the input array, with loop invariants to write for the proof to go through. Being able to execute these loop invariants as regular assertions made me quite confident that I had not written wrong assertions, before I even start proving something.

Hope to see even more participants at the next software verification competition, either VSTTE’s one or VerifyThis!