Software Model Checking without Source Code
Chaki, James Ivers,
Proceedings of the 1st NASA Formal Methods Symposium (NFM),
page 36-45, April 6-8, 2009.
We present a framework, called AIR, for verifying safety properties
of assembly language programs via software model checking. AIR
extends the applicability of predicate abstraction and counterexample
guided abstraction refinement to the automated verification of
low-level software. By working at the assembly level, AIR allows
verification of programs for which source code is unavailable--such as
legacy and COTS software--and programs that use features--such as
pointers, structures, and object-orientation--that are problematic for
source-level software verification tools. In addition, AIR makes no
assumptions about the underlying compiler technology. We have
implemented a prototype of AIR and present encouraging results on
several non-trivial examples.