Bounded model checking is a variant of model checking.
Following the terminology in section 3.1 of bornholt:oopsla:2018, bounded model-checking is a form of symbolic evaluation where all paths are followed at a time.
The benefit of following all paths at once is that it avoids the path explosion problem seen in symbolic execution.
The disadvantage of following all paths at once is that this requires that states are merged at join points so many calculations involve symbolic values requiring the use of a solver to resolve.
Notes related to Bounded model-checking
Bounded verification, CBMC verifier, Swarm verification, Symbolic evaluation, Symbolic execution, Verification performance of code, Verification profiling of code, Verifier performance
Papers related to Bounded model-checking
- Symbolic model checking without BDDs [biere:tacas:1999]
- Finding code that explodes under symbolic evaluation [bornholt:oopsla:2018]
- Model checking: Algorithmic verification and debugging [clarke:cacm:2009]
- A tool for checking ANSI-C programs [clarke:tacas:2004]
- Model checking boot code from AWS data centers [cook:cav:2018]
- Software model checking [jhala:compsurv:2009]
- Efficient state merging in symbolic execution [kuznetsov:pldi:2012]
- LLBMC: Bounded model checking of C and C++ programs using a compiler IR [merz:vstte:2012]
- End-to-end verification of ARM processors with ISA-formal [reid:cav:2016]
- Towards making formal methods normal: meeting developers where they are [reid:hatra:2020]
- Defining interfaces between hardware and software: Quality and performance [reid:phd:2019]
- Scaling symbolic execution using ranged analysis [siddiqui:oopsla:2012]
- A lightweight symbolic virtual machine for solver-aided host languages [torlak:pldi:2014]
- Scalable error detection using boolean satisfiability [xie:popl:2005]