Cookbook for Applying Formal Methods in Industry

If you read a bit of French, you’ll be happy to know that Hermes Publishing has just issued the first of a three-volume series on Utilisations industrielles des techniques formelles (use of formal methods in industry). This first volume is concerned with abstract interpretation techniques and tools. As such, we at AdaCore contributed a chapter on the static analyzer CodePeer that we develop. Other chapters describe the use of other tools based on abstract interpretation and formal methods in a broader sense: Polyspace, Astrée, Frama-C, etc. I liked in particular the discussion about the use of formal methods for in DO-178C context, and the combination of formal verification and testing, in chapter 7 by Dassault Aviation Méthodes formelles et conformité au standard DO-178C/ED-12C en aéronautique. We do have solutions in project Hi-Lite to some of the problems they raised.

Here is the book, that you can also find at your preferred web merchant.

The two remaining books on the B methods, Scade, SPARK and others, should be published by the end of 2011. An English version of the three books is expected to be published in 2012.