[Haskell-cafe] ANN: afv-0.0.0

[Tom Hawkins]

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
k-induction 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
- non-unique 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 language-c
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/language-c
[4] http://hackage.haskell.org/package/yices