The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform. - BAUDIN, PATRICK; BOBOT, FRANÇOIS; BÜHLER, DAVID; CORRENSON, LOÏC; KIRCHNER, FLORENT; KOSMATOV, NIKOLAI; MARONEZE, ANDRÉ; PERRELLE, VALENTIN; PREVOSTO, VIRGILE; SIGNOLES, JULIEN; WILLIAMS, NICKY (Communications of the ACM, 2021)
The article criticizes aspects of the computer programming language C with a focus on the use of the Frama-C26 code analysis platform to proactively address illegal programs written in C. A gallery of Frama-C26 plug-ins for varying analyses and use cases including undefined behavior, verification of functional properties, and test case generation is provided. The use of Frama-C26 in education as well as industrial collaboration is outlined.