Applying symbolic bounded model checking to the 2012 RERS greybox challenge

作者：Morse Jeremy; Cordeiro Lucas; Nicole Denis; Fischer Bernd^*

来源：International Journal on Software Tools for Technology Transfer, 2014, 16(5): 519-529.

DOI：10.1007/s10009-014-0335-0

• Program verification
• Symbolic bounded model checking
• Verification competition

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.

• 出版日期2014-10