kirancodes.me
To Proof Maintenance & Beyond!
ASE 2018

ESBMC 5.0: an industrial-strength C model checker

Mikhail Y. R. Gadelha, Felipe R. Monteiro, Jeremy Morse, Lucas C. Cordeiro, Bernd Fischer, Denis A. Nicole

PDFDOI 10.1145/3238147.3240481dblp

Abstract

ESBMC is a mature, permissively licensed open-source context-bounded model checker for the verification of single- and multi-threaded C programs. It can verify both predefined safety properties (e.g., bounds check, pointer safety, overflow) and user-defined program assertions automatically. ESBMC provides C++ and Python APIs to access internal data structures, allowing inspection and extension at any stage of the verification process. We discuss improvements over previous versions of ESBMC, including the description of new front- and back-ends, IEEE floating-point support, and an improved k-induction algorithm. A demonstration is available at https://www.youtube.com/watch?v=YcJjXHlN1v8 .

BibTeX
@inproceedings{Gadelha-al:ASE18,
  author    = {Mikhail Y. R. Gadelha and
               Felipe R. Monteiro and
               Jeremy Morse and
               Lucas C. Cordeiro and
               Bernd Fischer and
               Denis A. Nicole},
  title     = {{ESBMC} 5.0: an industrial-strength C model checker},
  booktitle = {ASE},
  pages     = {888--891},
  publisher = {{ACM}},
  year      = {2018},
}

Related papers