Bug-Finder:
Enhanced Error Detection in Concurrent Computer Programs
Bug finding is one of the most important application areas of
computer science in general and software model checking
in particular. Current technology like embedded systems and
internet programs, ask for a suitable combination of
program execution and verification.
The sheer size of the reachable state space of realistic models
imposes tremendous challenges on the algorithmics of model checking
technology. Complete exploration of the state space is often
unfeasible and approximations are needed. Also, the error trails
reported by depth-first search model checkers are often exceedingly
lengthy -- in many cases they consist of mutliple thousands of
computation steps which greatly hampers error interpretation. In the
meantime, state space exploration is a central aspect of AI, and the
AI community has a long and impressive line of research in developing
and improving search algorithms over very large state spaces under a
broad range of assumptions.
Therefore, the interest on applying AI-based search techniques to
software model checking grew and was applied in different domains:
Java and C++ programs, real-time systems, hardware circuits. In some
cases ressearch produced or extended verification tools with heuristic
search capabilities. We mention, among others, HSF-SPIN (an extension
of the SPIN model checker), Java Path Finder and StEAM.
Usually one distinguishes various aspects in the verification of
systems. First, due to the complexity of concurrent and distributed
systems, errors are very likely to appear and one desires to find them
as quickly as possible. Next, one looks for short error trails, easier
to understand than longer ones. Since the requirements of the these
two phases are not the same, different heuristic search strategies
apply.