DIMACS TR: 96-15
Workshop Summary: Computational and Complexity Issues in Automated Verification
Authors: R. Brayton, A. Emerson, J. Feigenbaum
ABSTRACT
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