Tag - alt-ergo

Entries feed - Comments feed

Last entries

Introduction aux méthodes formelles actualisée

Comme en 2010 et 2011, j'ai faire une intervention de 2h pour présenter les méthodes formelles à l'ESIR, école d'ingénieur de Rennes 1. J'ai un peu actualisé la présentation, je pense qu'elle est plus illustrée et j'ai introduit quelques démonstrations d'utilisation des outils. La présentation est disponible en PDF ou en source au format PowerPoint (licence Art Libre, sauf pour les illustrations, que j'ai pioché à droite et à gauche sur le web).

Note pour les libristes : la plupart des logiciels mentionnées sont libres.

Looking for a C software for Formal Verification

As you probably know, I'm a huge fan of Formal Methods: use appropriate Mathematics and tools to ensure a program is correct in all possible situations. In other words, bug free software... well, sort of. :-)

The interesting side of this is that tools to apply Formal Methods have improved a lot and most of them are now Free Software. I'm maintaining a list of Free Software tools for Formal Methods (it is a wiki, you can update it!).

I would like to make an experiment with Frama-C and its plugins, especially Jessie. Frama-C is a framework for static analysis of C programs developed at CEA. Combined with the Why and Alt-Ergo tools, you can prove some properties on real C code (absence of integer underflow or overflow, absence of out-of-bound accesses, absence of NULL pointer de-referencing, program's specific properties, etc.). All those tools are Free Software and are developed in OCaml. And they now are available in Debian and Ubuntu!

I made a simple experiment last year but I would like to make a more elaborated one.

Therefore, I'm looking for a piece of C code with following criteria:

  • Free Software: I'm interested in improving software for the whole humankind; ;-)
  • Pure C code, no C++. If there is some assembly, I could work around for example by re-writting corresponding C function;
  • Code of moderate size, a few thousands line at most. It could be a sub-module or subset of a bigger code;
  • Code using mostly integers and pointers, few strings (aka char *)[1];
  • Verifying some properties on this code would be "interesting". Several possible reasons: for security or safety reasons, because the code is used in an embedded platform on which modifications are difficult once in production or simply because this code is used a lot.

If you know some software that fills those criteria, let me know through a comment or at dmentre@linux-france.org!


[1] Frama-C is a bit slow to handle strings and it can become cumbersome.