Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

First Annual IEEE Symposium on

Logic in Computer Science (LICS 1986)

Paper: An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report) (at LICS 1986)

Winner of the Test-of-Time Award in 2006
Authors: Moshe Y. Vardi Pierre Wolper

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 automaton 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 algortihms. We use this approach to extend model checking to probabilistic concurrent finite-state programs.

BibTeX

  @InProceedings{VardiWolper-AnAutomataTheoretic,
    author = 	 {Moshe Y. Vardi and Pierre Wolper},
    title = 	 {An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {332--344 },
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski