ESBMC 5.0: An industrial-strength C model checker

Mikhail Ramalho, Felipe R. Monteiro, Jeremy Morse, Lucas Cordeiro, Bernd Fischer, Denis Nicole

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

780 Downloads (Pure)


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 safety (e.g., bounds check, pointer safety, overflow) and user-defined (as asserts in the program) properties 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
Original languageEnglish
Title of host publication33rd IEEE/ACM International Conference on Automated Software Engineering
Publication statusPublished - 2018


Dive into the research topics of 'ESBMC 5.0: An industrial-strength C model checker'. Together they form a unique fingerprint.

Cite this