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.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Bounded model checking and abstract interpretation of large C codebases


    Beteiligte:


    Erscheinungsdatum :

    01.06.2017


    Format / Umfang :

    522432 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    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

    Freier Zugriff

    Model checking large software specifications

    Chan, W. / Anderson, R.J. / Beame, P. et al. | Tema Archiv | 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