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

Abstract

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
Volume16
Issue number5
DOIs
Publication statusPublished - Oct 2014

Keywords

  • Program verification
  • Symbolic bounded model checking
  • Verification competition

Fingerprint

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