Software model checking without source code
Chaki, James Ivers,
Innovations in Systems and Software Engineering (ISSE), volume 6,
number 3, page 233-242, September 2010.
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.