Efficient SAT-based Bounded Model Checking for Software Verification

Efficient SAT-based Bounded Model Checking for Software Verification

This talk discusses our methodology for formal analysis and automatic verification of software programs. It is currently applicable to a large subset of the C programming language. We consider reachability properties, in particular whether certain statements are reachable in the source code. We perform this analysis via a translation to a Boolean representation based on modeling basic blocks. The program is then analyzed by a backend SAT-based bounded model checker, where each unrolling is mapped to one step in a block-wise execution of the program.

Dr. Zijiang Yang is an Assistant Professor of Computer Science at
Western Michigan University. His primary research interest is formal
verification and its application in hardware and software designs. He
received his Ph.D. from the University of Pennsylvania and M.S. from
Rice University, both in Computer Science. Before joining WMU, Dr. Yang
was an associate research staff member at NEC Laboratories