In contrast to hardware which is finite-state and based on
relatively few ample principles, software systems generally
give rise to infinite state spaces, and are described in
terms of programming languages involving rich semantical
concepts. The challenges of software verification can be
addressed only by a combined effort of different
communities including, most notably, model checking,
theorem proving, symbolic computation, static analysis,
compilers, and abstract interpretation. We focus on a
recent family of tools which use predicate abstraction and
theorem proving to extract a finite state system amenable
to model checking.
© 2002-2003 Kurt Gödel Society, Norbert Preining.