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