### DIMACS Workshop on Computational and Complexity Issues in Automated Verification

#### March 25 - 28, 1996

DIMACS Center, Rutgers University, Piscataway, NJ

**Organizers:**
**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.