
Hi,
Here is the first release of Atom's Formal Verifier (AFV) [1], a tool
intended to verify Atom  or human  generated C code. With the
help of the Yices SMT solver [2], AFV uses bounded model checking and
kinduction to verify assertions in iteratively called C functions,
such as an embedded control loop. For each assertion in a design, AFV
will return a pass, a fail, or an inconclusive result  or it will
die trying. In addition to Yices, AFV needs GCC for C preprocessing.
This is a very early release. There are many things missing including
counter example generation, finite precision modeling, and basic model
reduction. And they is a chance  say about 100%  that there are
bugs with the modeling transformations. In addition, the list of
unsupported C syntax is embarrassingly long:
 recursive functions
 nonunique top level names (e.g. top level names hidden with static)
 loops
 switch statements
 pointers
 arrays
 type casting
 non void functions
 functions with arguments
 structs
 enums
 unions
 typedefs
Still, AFV works well for the handful of tests I have tried so far.
AFV comes with a simple example. To run:
$ afv example # This generates afv.h and example.c shown below...
// Provides assert and assume functions.
#include "afv.h"
// Periodic function for verification. Implements a simple rolling counter.
void example () {
// The rolling counter.
static int counter = 0;
// Assertions.
GreaterThanOrEqualTo0: assert(counter >= 0); // The 'counter'
must always be greater than or equal to 0.
LessThan10: assert(counter < 10); // The 'counter'
must always be less than 10.
// Implementation 1.
if (counter == 10)
counter = 0;
else
counter++;
// Implementation 2.
// if (counter == 9)
// counter = 0;
// else
// counter = counter + 1;
// Implementation 3.
// if (counter >= 9)
// counter = 0;
// else
// counter++;
// Implementation 4.
// if (counter >= 9  counter < 0)
// counter = 0;
// else
// counter++;
// Implementation 5.
// counter = (counter + 1) % 10;
}
To run the verification on the example:
$ afv verify example k 20 example.c # Which returns...
parsing example.c ...
verifying assertion example.GreaterThanOrEqualTo0.assert ...
inconclusive: unable to proved step up to max k = 20
verifying assertion example.LessThan10.assert ...
FAILED: disproved basis in k = 11
These results state AFV was unable to prove the
"GreaterThanOrEqualTo0" assertion and it disproved the "LessThan10"
assertion. The different implementations in the example yield
different results.
Any feedback or questions are more than welcome.
I would like to thank Benedikt Huber and friends for the languagec
library [3], Ki Yung Ahn for the yices library [4], and the folks at
SRI for their work on the Yices SMT solver. Without these tools and
libraries, AFV would not have been possible.
Tom
[1] http://hackage.haskell.org/package/afv
[2] http://yices.csl.sri.com/
[3] http://hackage.haskell.org/package/languagec
[4] http://hackage.haskell.org/package/yices
_______________________________________________
HaskellCafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskellcafe

