C Bounded Model Checker
Bounded model checker
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.
01Applications
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.
Sources and credits
This article is adapted from the Wikipedia article “C Bounded Model Checker”, written by its contributors and licensed under CC BY-SA 4.0. Fathomly has changed the layout, removed citation markers, navigation and maintenance notices, and adjusted punctuation. This adapted version is shared under the same license. For references, see the original article.
Fathomly is not affiliated with or endorsed by the Wikimedia Foundation. Spotted a problem? Tell us.