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
01.06.2017
522432 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
Applied Bounded Model Checking for Interlocking System Designs
British Library Conference Proceedings | 2014
|Model checking large software specifications
Tema Archiv | 1997
|Space Software Validation Using Abstract Interpretation
British Library Conference Proceedings | 2009
|