C Bounded Model Checker

The C Bounded Model Checker is a bounded model checker for computer programs written in C. It was the first such tool.
CBMC has participated in the Competition on Software Verification in the years 2014–2022. It came in first in at least one category in 2014, 2015, and 2017.

Applications

CBMC has been used to verify C code at Amazon Web Services. It is used as model checker in the Kani and Crust verifiers for Rust, and the JBMC bounded model checker for Java.