A Tutorial on C Bounded Model Checker (CBMC)

Daniel Kroening, Amazon Web Services

VeTSS Summer School 2023

INTRODUCTION:

CBMC is a bounded model checker for C programs that has been developed since 2001. Since then, it has grown considerably beyond its original use-case, single-threaded embedded software written in C, and covers test-input generation, Java, Rust, and proof using contracts. The tutorial covers the basics of encoding software into logic, the basics of solving the resulting first-order verification conditions, and offers an outlook on contemporary research questions including unbounded proofs using Horn-clause encodings.

SPEAKER:

Daniel Kroening is a scientist at Amazon Web Services (AWS). He was a Professor of Computer Science at the Department of Computer Science at the University of Oxford until 2020, where he led the Systems Verification Group. He is the co-founder of Diffblue, a university spin-out that automates software engineering tasks. He has 15 years experience building software verification tools and is the primary author of the CBMC verification framework.