The seminar is concerned with guided and counter-example driven exploration in software model checking.
Heuristic guided search techniques have first been proposed in the area of Artificial Intelligence where they have been used quite successfully in solving complex planning and scheduling problems. On the other hand, Model Checking has evolved into one of the most successful verification techniques. Examples range from mainstream applications such as protocol validation, software model checking and embedded systems verification to exotic areas such as business workflow analysis, scheduler synthesis and planning. Model checking technology has also been proven to be effective in automated test case generation.
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.
In this context, we study directed search in explicit state model checking. evaluate the combination of heuristic search with bit-state hashing, iterative deepening, symmetry and partial-order reduction, external search, genetic algorithms, just to name a few.
Stefan Edelkamp, Alberto Lluch Lafuente, Stefan Leue: Directed Explicit Model Checking with HSF-SPIN, Proceedings 8th International SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science, Springer LNCS, Toronto, 2001. Download: http://www.inf.uni-konstanz.de/soft/research/publications/pdf/SPINSubmission.pdf
Alex Groce, Willem Visser. Model checking Java programs using structural heuristics International Symposium on Software Testing and Analysis archive Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis table of contents, Roma, Italy, pp 12 - 21, 2002 www.cs.cmu.edu/~agroce/sttt04.pdf
P. Godefroid, N. Klarlund, K. Sen. DART: Directed Automated Random Testing Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, Chicago, IL, USA, pp 213-223, 2005 http://cm.bell-labs.com/who/god/public_psfiles/pldi2005.pdf
C. Cadar, D. Engler Proceedings of the 12th International SPIN Workshop on Model Checking of Software (invited paper) San Francisco, CA, August 2005 www.stanford.edu/~engler/spin05.pdf
C. Cadar, V. Ganesh, P.M. Pawlowski, D.L. Dill, D. R. Engler. XE: Automatically Generating Inputs of Death, (postscript) 13th ACM Conference on Computer and Communications Security, 2006. http://www.stanford.edu/~engler/exe-ccs-06.pdf
L. Zhang, C.F. Madigan, M.H. Moskewicz Efficient Conflict Driven Learning in a Boolean Satisfiability Solver (2001) Proceedings of the International Conference on Computer Aided Design (ICCAD), San Jose, California, 11 2001. http://citeseer.ist.psu.edu/article/zhang01efficient.html
Paper discussing MiniSat (The winner of most SAT competitions) http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/cgi/MiniSat.ps.gz.cgi
N. Een and A. Biere. Effective Preprocessing in SAT through Variable and Clause Elimination, SAT 2005 proceedings. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/Main.html