This paper presents a methodology allowing the execution of Bounded Model Checking (via CBMC) and Abstract Interpretation (via Frama-C) analyses on large, real case, C codebases. Then the paper shows some of the results that can nowadays be achieved with relatively new tools like Clang Static Analyzer and Facebook Infer. Finally, a brief introduction on SonarQube and how it can be used to display and monitor the analyses results is given.
Bounded model checking and abstract interpretation of large C codebases
2017-06-01
522432 byte
Conference paper
Electronic Resource
English
Applied Bounded Model Checking for Interlocking System Designs
British Library Conference Proceedings | 2014
|Model checking large software specifications
Tema Archive | 1997
|Space Software Validation Using Abstract Interpretation
British Library Conference Proceedings | 2009
|