CBMC is a bounded model-checker for C and C++ programs.
Papers related to CBMC verifier
- Software verification: Testing vs. model checking [beyer:hvc:2017]
- Code-level model checking in the software development workflow [chong:icse:2020]
- A tool for checking ANSI-C programs [clarke:tacas:2004]
- FShell: Systematic test case generation for dynamic analysis and measurement [holzer:cav:2008]
- TracerX: Dynamic symbolic execution with interpolation [jaffar:arxiv:2020]
- Software model checking [jhala:compsurv:2009]
- Crust: A bounded verifier for Rust [toman:ase:2015]
- Scalable error detection using boolean satisfiability [xie:popl:2005]