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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Bounded model checking and abstract interpretation of large C codebases


    Contributors:


    Publication date :

    2017-06-01


    Size :

    522432 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Applied Bounded Model Checking for Interlocking System Designs

    Haxthausen, A.E. / Peleska, J. / Pinger, R. | British Library Conference Proceedings | 2014


    Functional Abstract Interpretation

    Graf, Sebastian | TIBKAT | 2025

    Free access

    Model checking large software specifications

    Chan, W. / Anderson, R.J. / Beame, P. et al. | Tema Archive | 1997


    (abstract) Automated Constraint Checking of Spacecraft Command Sequences

    Horvath, Joan / Alkalaj, Leon / Schneider, Karl et al. | NTRS | 1994


    Space Software Validation Using Abstract Interpretation

    Bouissou, O. / Conquet, E. / Cousot, P. et al. | British Library Conference Proceedings | 2009