Model Checking of Predicate Abstracted Programs without BDDs

May 20, 2005
Michael Hsiao | Virginia Tech

In recent years, software model checking has been offered as a viable solution to the “bug hunt” in software. Although only in its infancy, software model checking has shown promise in tackling this very difficult problem. In this talk, emphasis will be placed on the model checking within the verification process, whereby the abstracted Boolean program (modeled as a finite transition system) undergoes scrutiny. Conventional BDD-based model checking tools may suffer from space and/or computational limitations for large state spaces. Instead, we offer a new model checking paradigm that is based on SAT rather than BDDs.

While there has been some work on SAT-based state space traversal, they have been centered on the concept of “blocking clauses”, which is a direct derivation from conflict-driven learning in SAT solvers. On the other hand, we offer a completely different way of learning, in which knowledge is obtained from successes rather than conflicts. In our framework, equivalent search spaces form the knowledge base over which learning is performed. With our approach, significant space and time reductions are achieved, where conflict-driven methods could not. Our initial findings demonstrated that several orders of magnitude reduction in computation effort can be obtained.

Speaker Details

Michael S. Hsiao received the B.S. in computer engineering with highest honors from the University of Illinois at Urbana-Champaign in 1992, and M.S. and Ph.D in electrical engineering in 1993 and 1997, respectively, from the same university. During his studies, he was recipient of the Digital Equipment Corp. Fellowship, McDonnell Douglas Scholarship, and Semiconductor Research Corp. Research Assistantship. Currently, Michael is an Associate Professor in the Department of Electrical and Computer Engineering at Virginia Tech.Michael is a recipient of the National Science Foundation CAREER Award. He has graduated more than 20 MS and PhD students, with whom he has published more than 90 journal and conference papers. His current research focuses on verification, testing, diagnosis, and power management of complex digital systems.