Paper

An Automata-Theoretic Approach to Automatic Program Verification

Publication Date:
July 1986

paper Menu

Abstract

We describe an automata-theoretic approach to automatic verification of concurrent finite-state programs by model checking.  The basic idea underlying this approach is that for any temporal formula we can construct an automation that accepts precisely the computations that satisfy the formula.  The model-checking algorithm that results from this approach is much simpler and cleaner than tableau-based algorithms.  We use this approach to extend model-checking to probabilistic concurrent finite-state programs.

Description

Published in the proceedings of the 1st Symposium on Logic in Computer Science, 1986