[Chair]  [Computer Science Department (FBI)]  [University Dortmund] 

Project Group Application

Final Report



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.


Stefan Edelkamp

Bug-Finder is being developed by Stefan Edelkamp, Tilman Mehler and Shahid Jabbar and by the PG.
Thanks to Peter Leven for code organizes the memory pool