Article published FRAMA-C
Software under the magnifying glass
Verification of correct software operation is a major industrial issue. Formally analysing the source code of a piece of software and its properties (errors, resource requirements, run time, functional contracts, etc.) is an economic and technically feasible activity. Frama-C is the result of a collaboration between the CEA LIST and INRIA, and is an open software platform enabling the collaboration of source code analysis modules. It provides a representation of the program to be analysed and a means of attaching demonstrated properties or properties to be demonstrated; Numerous extensions are provided to help test these properties. The goal is to popularise Frama-C so that potential users familiarise themselves with the possibilities that are offered by this type of tool and so that technology suppliers add other extensions, open or proprietary, in order for the offering to expand.
http://frama-c.cea.fr
