Verification of concurrent programs: The automata-theoretic framework
From MaRDI portal
Publication:2277249
DOI10.1016/0168-0072(91)90066-UzbMATH Open0725.03013MaRDI QIDQ2277249FDOQ2277249
Publication date: 1991
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Recommendations
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking
- Temporal logics for concurrent recursive programs: satisfiability and model checking
- scientific article; zbMATH DE number 4128366
- Realizability of Concurrent Recursive Programs
terminationcorrectnessacceptance conditionsrecursive automata on infinite treesrecursive infinitary temporal logicverification of concurrent and nondeterministic programs
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Cites Work
- The complexity of propositional linear temporal logics
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The temporal semantics of concurrent programs
- Temporal logic can be more expressive
- Fairness and related properties in transition systems - a temporal logic to deal with fairness
- Propositional dynamic logic of looping and converse is elementarily decidable
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Title not available (Why is that?)
- Ten Years of Hoare's Logic: A Survey—Part I
- Title not available (Why is that?)
- Countable nondeterminism and random assignment
- Title not available (Why is that?)
- Programming as a Discipline of Mathematical Nature
- The complementation problem for Büchi automata with applications to temporal logic
- Propositional dynamic logic of nonregular programs
- Theories of automata on \(\omega\)-tapes: a simplified approach
- Proving Liveness Properties of Concurrent Programs
- Ten years of Hoare's logic: A survey. II: Nondeterminism
- Title not available (Why is that?)
- Proof rules and transformations dealing with fairness
- A proof rule for fair termination of guarded commands
- A Weaker Precondition for Loops
- Fair termination revisited - with delay
- On verifying that a concurrent program satisfies a nondeterministic specification
- Verifying temporal properties without temporal logic
- Title not available (Why is that?)
- Adequate proof principles for invariance and liveness properties of concurrent programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Infinite trees, markings, and well-foundedness
Cited In (40)
- Uniform strategies, rational relations and jumping automata
- Formalization and correctness of a concurrent linear hash structure algorithm using nested transactions and I/O automata
- Verifying Concurrent Systems with Symbolic Execution
- Robin Milner 1934--2010
- Automata-based verification of programs with tree updates
- On the complexity of verifying concurrent transition systems
- Infinite trees, markings, and well-foundedness
- Realizability of Concurrent Recursive Programs
- Liveness-Preserving Atomicity Abstraction
- Recognizing safety and liveness
- Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach
- Title not available (Why is that?)
- Computability and realizability for interactive computations
- Automated Verification of Concurrent Search Structures
- Liminf progress measures
- Verification of sequential and concurrent programs
- Quantum temporal logic and reachability problems of matrix semigroups
- Automata for true concurrency properties
- Formal verification of language-based concurrent noninterference
- Parameterized Verification of Communicating Automata under Context Bounds
- On control of systems modelled as deterministic Rabin automata
- Model checking duration calculus: a practical approach
- On the refinement of liveness properties of distributed systems
- Verification by augmented abstraction: The automata-theoretic view
- A compositional approach to CTL\(^*\) verification
- Verification by augmented finitary abstraction
- A GENERAL NOTION OF UNIFORM STRATEGIES
- Title not available (Why is that?)
- Automatically verifying temporal properties of pointer programs with cyclic proof
- On the role of automated theorem proving in the compile-time derivation of concurrency
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
- Bridging the gap between fair simulation and trace inclusion
- Deductive verification of alternating systems
- Verification of parameterized concurrent programs by modular reasoning about data and control
- Towards a grand unification of Büchi complementation constructions
- Streett Automata Model Checking of Higher-Order Recursion Schemes
- Automatic and hierarchical verification for concurrent systems
- Caper
- Verifying a scheduling protocol of safety-critical systems
- Inference of ranking functions for proving temporal properties by abstract interpretation
This page was built for publication: Verification of concurrent programs: The automata-theoretic framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2277249)
