Applying symbolic bounded model checking to the 2012 RERS greybox challenge

Jeremy Morse, Lucas Cordeiro, Denis Nicole, Bernd Fischer

Research output: Contribution to journalArticlepeer-review


We describe the application of ESBMC, a symbolic bounded model checker for C programs, to the 2012 RERS greybox challenge. We checked the reachability properties via reachability of the error labels, and the behavioral properties via a bounded LTL model checking approach. Our approach could solve about 700 properties for the small and medium problems from the offline phase, and scored overall about 5,000 marks but still ranked last in the competition.
Original languageEnglish
Pages (from-to)519-529
JournalInternational Journal on Software Tools for Technology Transfer
Issue number5
Publication statusPublished - Oct 2014


  • Program verification
  • Symbolic bounded model checking
  • Verification competition


Dive into the research topics of 'Applying symbolic bounded model checking to the 2012 RERS greybox challenge'. Together they form a unique fingerprint.

Cite this