C Bounded Model Checker
Jump to navigation
Jump to search
| C Bounded Model Checker | |
|---|---|
| Repository |
|
| Engine | |
| Website | www |
In the context of computer science, the C Bounded Model Checker (CBMC) is a bounded model checker for C programs.[1] It was the first such tool.[2]
CBMC has participated in the Competition on Software Verification (SV-COMP) in the years 2014–2022.[3] It came in first in at least one category in 2014, 2015, and 2017.
Applications
[edit | edit source]CBMC has been used to verify C code at Amazon Web Services.[4][5] It is used as model checker in the Kani and Crust verifiers for Rust,[6] and the JBMC bounded model checker for Java.[7]
References
[edit | edit source]- ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^
- 2020: Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- 2021: Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- 2022: Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^
- For Kani: Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- For Crust: Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).