DIMACS TR: 96-15

Workshop Summary: Computational and Complexity Issues in Automated Verification

Authors: R. Brayton, A. Emerson, J. Feigenbaum


The correctness of computer hardware and software is an area of growing theoretical interest and practical importance. It is now widely acknowledged that effective reasoning about program correctness requires: (i) the use of appropriate formalisms, such as temporal logic or automata, for rigorously specifying correct behavior, and (ii) the use of mechanical reasoning algorithms, such as model checkers, to permit proofs of correctness to be constructed automatically that could not reasonably be constructed by hand owing to the intractable amount of tedious detail. A principal limiting factor in automated verification is the computational complexity of various associated mechanical reasoning problems; this complexity might be prohibitively high because of the combinatorial state explosion problem, which appears in many guises.

The DIMACS Workshop on Computational and Complexity Issues in Automated Verification, held at Rutgers University on March 25-28, 1996, and organized by Bob Brayton (University of California at Berkeley), Allen Emerson (University of Texas), Joan Feigenbaum (AT&T Research), featured both theoretical and practical work in this important area of computer science. This report contains short abstracts of all talks given at the workshop, as well as pointers to sources of more information.

Paper Available at: ftp://dimacs.rutgers.edu/pub/dimacs/TechnicalReports/TechReports/1996/96-15.ps.gz

DIMACS Home Page