Bounded model checking is a variant of model checking.
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
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]