C Bounded Model Checker
In-game article clicks load inline without leaving the challenge.
The C Bounded Model Checker (CBMC) 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 (SV-COMP) 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.