Verification of concurrent programs: The automata-theoretic framework

DOI10.1016/0168-0072(91)90066-UzbMath0725.03013MaRDI QIDQ2277249

Moshe Y. Vardi

Publication date: 1991

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

correctnessterminationacceptance conditionsrecursive automata on infinite treesrecursive infinitary temporal logicverification of concurrent and nondeterministic programs

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Recognizing safety and liveness, On control of systems modelled as deterministic Rabin automata, Infinite trees, markings, and well-foundedness, Towards a grand unification of Büchi complementation constructions, Verifying a scheduling protocol of safety-critical systems, Liminf progress measures, Deductive verification of alternating systems, Model checking duration calculus: a practical approach, Liveness-Preserving Atomicity Abstraction, A GENERAL NOTION OF UNIFORM STRATEGIES, Inference of ranking functions for proving temporal properties by abstract interpretation, Bridging the gap between fair simulation and trace inclusion, A compositional approach to CTL\(^*\) verification, Verification by augmented abstraction: The automata-theoretic view, Automatically verifying temporal properties of pointer programs with cyclic proof, On the refinement of liveness properties of distributed systems, Streett Automata Model Checking of Higher-Order Recursion Schemes, Verification by augmented finitary abstraction, Computability and realizability for interactive computations, Uniform strategies, rational relations and jumping automata

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Propositional dynamic logic of nonregular programs
• Adequate proof principles for invariance and liveness properties of concurrent programs
• Fair termination revisited - with delay
• Proof rules and transformations dealing with fairness
• Ten years of Hoare's logic: A survey. II: Nondeterminism
• The complementation problem for Büchi automata with applications to temporal logic
• Infinite trees, markings, and well-foundedness
• On verifying that a concurrent program satisfies a nondeterministic specification
• The temporal semantics of concurrent programs
• Fairness and related properties in transition systems - a temporal logic to deal with fairness
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Temporal logic can be more expressive
• Propositional dynamic logic of looping and converse is elementarily decidable
• A proof rule for fair termination of guarded commands
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Countable nondeterminism and random assignment
• The complexity of propositional linear temporal logics
• Verifying temporal properties without temporal logic
• Ten Years of Hoare's Logic: A Survey—Part I
• Proving Liveness Properties of Concurrent Programs
• A Weaker Precondition for Loops
• Programming as a Discipline of Mathematical Nature