 |
|
||||||||||||||
 |
 |
 |
 |
 |
 |
 |
 |
|
|||||||
|
|
||||||||||||||
|
|
||||||||||||||
|
|
||||||||||||||
Edmund M. Clarke
Department of Computer Science
Carnegie Mellon University
Abstraction Refinement in Software Model Checking
Abstract
Model checking is an automatic verification technique for state
transisiton systems. It was originally developed for finite state systems
and has been used successfully to verify complex hardware controllers and
communication protocols. The big challenge now is to adapt the method to
the verification of computer software. Because the state spaces involved
can very large or even infinite in this case, abstraction is crucial. I
will discuss recent work by my group on two abstraction techniques,
predicate abstraction and counterexample guided abstraction refinement,
that are used by almost all software model checkers.
