SMT-CBMC: a STM-based Bounded Model Checker

SMT-CBMC a bounded model checker for sequential programs. It generalizes the encoding technique developed and implemented in CBMC so to generate an SMT formula instead of a SAT formula. In this way SMT-CBMC leverages the stenghts of state-of-the-art SMT solvers, namely the ability to reason about complex data structures (e.g. numerical data, bit-vectors, lists, arrays).

SMT-CBMC has been developed in the AI-Lab at the University of Genova and has been partly supported by the Italian Ministry of University and Research, in the context of the PRIN Project no. 2003-097383.



The following people contributed to the development of SMT-CBMC: