CBMC implements bit-precise bounded model checking for C programs and has been developed and maintained for more than ten years. CBMC verifies the absence of violated assertions under a given loop unwinding bound. Other properties, such as SV-COMP's ERROR labels or memory safety properties are reduced to assertions via automated instrumentation. Only recently support for efficiently checking concurrent programs, including support for weak memory models, has been added. Thus, CBMC is now capable of finding counterexamples in all of SV-COMP's categories. As back end, the competition submission of CBMC uses MiniSat 2.2.0. © 2014 Springer-Verlag.
CITATION STYLE
Kroening, D., & Tautschnig, M. (2014). CBMC - C Bounded Model Checker (Competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8413 LNCS, pp. 389–391). Springer Verlag. https://doi.org/10.1007/978-3-642-54862-8_26
Mendeley helps you to discover research relevant for your work.