Verification of concurrent programs: the automata-theoretic framework

Annals of Pure and Applied Logic 51 (1-2):79-98 (1991)
  Copy   BIBTEX

Abstract

Vardi, M.Y., Verification of concurrent programs: the automata-theoretic framework, Annals of Pure and Applied Logic 51 79–98. We present an automata-theoretic framework to the verification of concurrent and nondeterministic programs. The basic idea is that to verify that a program P is correct one writes a program A that receives the computation of P as input and diverges only on incorrect computations of P. Now P is correct if and only if a program PA, obtained by combining P and A, terminates. We formalize this idea in a framework of ω-automata with a recursive set of states. This unifies previous works on verification of fair termination and verification of temporal properties

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Iterating semantic automata.Shane Steinert-Threlkeld & I. I. I. Thomas F. Icard - 2013 - Linguistics and Philosophy 36 (2):151-173.
Program verification: the very idea.James H. Fetzer - 1988 - Communications of the Acm 31 (9):1048--1063.
Fine-grained Concurrency with Separation Logic.Kalpesh Kapoor, Kamal Lodaya & Uday S. Reddy - 2011 - Journal of Philosophical Logic 40 (5):583-632.
Weak Cardinality Theorems.Till Tantau - 2005 - Journal of Symbolic Logic 70 (3):861 - 878.
Information-oriented computation with BABY-SIT.Erkan Tin & Varol Akman - 1996 - In Jerry Seligman & Dag Westerståhl (eds.), Logic, Language and Computation, Volume 1. Stanford, CA: Center for the Study of Language and Information Publications. pp. 19-34.
BABY-SIT: a computational medium based on situations.Erkan Tin & Varol Akman - 1993 - In Paul Dekker & Martin Stokhof (eds.), 9th Amsterdam Colloquium. Amsterdam, The Netherlands: Institute for Logic, Language and Computation.
Does one size fit all? Hurley on shared circuits.Alvin I. Goldman - 2008 - Behavioral and Brain Sciences 31 (1):27-28.
Timing diagrams: Formalization and algorithmic verification. [REVIEW]Kathi Fisler - 1999 - Journal of Logic, Language and Information 8 (3):323-361.
Automata for Epistemic Temporal Logic with Synchronous Communication.Swarup Mohalik & R. Ramanujam - 2010 - Journal of Logic, Language and Information 19 (4):451-484.

Analytics

Added to PP
2014-01-16

Downloads
30 (#519,519)

6 months
7 (#411,886)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

A Sound And Complete Deductive System For Ctl* Verification.Dov Gabbay - 2008 - Logic Journal of the IGPL 16 (6):499-536.
Generalisation of disjunctive sequences.Cristian S. Calude - 2005 - Mathematical Logic Quarterly 51 (2):120.

Add more citations

References found in this work

No references found.

Add more references