A Software Analysis Perspective

Frama-C is a source code analysis platform that aims at con- ducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive veri- fication, and testing, for safety- and security-critical software. Collabora- tive verification across cooperating plug-ins is enabled by their integra- tion on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.