Edmund M. Clarke (CMU), Bounded Model Checking in Hardware and Software

Bounded Model Checking (BMC) is already an important technique in hardware verification -- one that is actually used in industry. BMC can also be used in software verification as has been demonstrated by Kroening, et al in the CMBC model checker for ANSI C. I will review how it is used in both hardware and software, describe ongoing research on these topics in my group at CMU and speculate on important directions for future research dealing with BMC.