## Invited Paper: Automatic verification of finite-state concurrent systems (at LICS 1994)

**Edmund M. Clarke**

### Abstract

Logical errors in finite-state concurrent systems such as sequential circuit designs and communication protocols are an important
problem for computer scientists. A research group has developed a verification method called temporal logic model checking
for this class of systems. In this approach specifications are expressed in a propositional temporal logic, while circuits
and protocols are modeled as state-transition systems. An efficient search procedure is used to determine automatically if
a specification is satisfied by some transition system. The technique has been used to find subtle errors in a number of non-trivial
examples. During the last few years, the size of the state-transition systems that can be verified by model checking techniques
has increased dramatically. By representing transition relations implicitly using binary decision diagrams (BDDs), we have
been able to check some examples that would have required 10^{20} states with the original algorithm. Various refinements of the BDD-based techniques have pushed the state count up to 10^{100}. By combining model checking with various abstraction techniques, we have been able to handle even larger systems. We focus
on four of the most important directions for research: use of abstraction and symmetry to achieve an even greater reduction
in the size of the state-space that must be explored by this method; development of model checking techniques that can handle
parameterized designs without requiring each individual instance of the design to be verified; use of partial order semantics
to avoid the state explosion problem that can occur in loosely coupled systems when concurrency is modeled by interleaving;
determination of appropriate models and verification techniques for circuits and protocols with real-time constraints

### BibTeX

@InProceedings{Clarke-Automaticverificati, author = {Edmund M. Clarke}, title = {Automatic verification of finite-state concurrent systems}, booktitle = {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)}, year = {1994}, month = {July}, pages = {126}, location = {Paris, France}, note = {Invited Talk}, publisher = {IEEE Computer Society Press} }