DIMACS Workshop on Computational and Complexity Issues in Automated Verification

March 25 - 28, 1996
DIMACS Center, Rutgers University, Piscataway, NJ

Bob Brayton,University of California - Berkeley, brayton@ic.eecs.berkeley.edu
Allen Emerson, University of Texas, emerson@cs.utexas.edu
Joan Feigenbaum, AT&T Labs - Research, jf@research.att.com
Presented under the auspices of the DIMACS Special Year on Logic and Algorithms.

The correctness of computer hardware and software is an area of growing theoretical interest as well as practical importance. It is now widely acknowledged that the best way to reason about program correctness hinges on two criteria: (i) the use of appropriate formalisms, such as temporal logic or automata, for rigorously specifying correct behavior; (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 to automated verification is the computational complexity of various associated mechanical reasoning problems, which might be prohibitively high due to the combinatorial state explosion problem in various guises. The workshop will focus on such topics as the theoretical complexity as well as the practical efficiency of model checking algorithms and of testing satisfiability of logics, both in general and in applications-oriented special cases. Other methods for overcoming state explosion such as abstraction through the use of simulations and bisimulation relations are also important. Still other topics include the use of compositionality and modularity to simplify the construction of a correct program from correct constituent subprograms, program checking, testing and correcting, and program synthesis.

A portion of the workshop will be devoted to tools for verification and testing, evaluation of their strengths versus weaknesses, and reports on real experiences with industrial applications.

Next: Call for Participation
Workshop Index
DIMACS Homepage
Contacting the Center
Document last modified on November 2, 1998.