Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141–157. Springer, Heidelberg (2013)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using Bounded Model Checking. In: DAC, pp. 368–371 (2003)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kroening, D., Tautschnig, M. (2014). CBMC – C Bounded Model Checker. In: Ábrahám, E., Havelund, K. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2014. Lecture Notes in Computer Science, vol 8413. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54862-8_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-54862-8_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54861-1
Online ISBN: 978-3-642-54862-8
eBook Packages: Computer ScienceComputer Science (R0)