Last entries

Fri 17 Aug 2012

GNATprove tools available

Since end of July, a GPL release of GNATprove, the tools to make formal verification of Ada 2012 programs, is available.

One can now formally verify Ada programs using only Free Software! If you are interested, you can look at my previous attempt to verify a toy electronic booth program using GNATprove.

A proved toy electronic voting booth program in Ada

Three years ago, in March 2009, I wrote a toy electronic voting booth program in C language. The goal was to formally verify it using the Frama-C/Jessie framework. The program was short enough to be entirely understood in a short time but complex enough (with arrays, integer arithmetic, strings, I/O, ...) to exert formal verification techniques.

Since then, Hi-Lite project has started, with the aim of providing tools to mix formal verification and tests in the same program, following Design-by-Contract approach. Hi-Lite tools are supporting two languages, C extended with ACSL, Frama-C's specification language, and Ada 2012 that now supports Pre-conditions and Post-conditions on procedures.

Thus I attempted to do a similar work using AdaCore's GNATprove verification tool. The result is now publicly available as ada-evoting-0.2, under a very liberal BSD license, thanks to the help of Claire Dross and Yannick Moy of AdaCore. They helped me write the last invariants and fix the last bugs. All the Verification Conditions (VC) can now be automatically proved using Alt-Ergo, an SMT solver available as free software and developed by ProVal research team of INRIA/LRI.

The program has been verified with latest release of GNATprove. GNATprove is not yet publicly available but Yannick announced that a GPL release of it should occur before the end of this month. So, in a short time frame one should have all needed free software (IDE, compiler, VC generator and automatic prover) to write and prove Ada programs, with a small example of its use. Nice isn't it? :-)

There still a lot of things to do on that small program, like using GNATtest to test it in the usual way or make a SPARK version to formally verify it with SPARK tools (of which a new GPL edition should be release shortly). But, as usual, days are not long enough. ;-)

PS: Ada is very nice to write such kind of low level software. I haven't used it for more than 10 years but I really enjoyed using again the language.