Verification of concurrent programs: The automata-theoretic framework
From MaRDI portal
Publication:2277249
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
Cites work
- scientific article; zbMATH DE number 3839297 (Why is no real title available?)
- scientific article; zbMATH DE number 3965428 (Why is no real title available?)
- scientific article; zbMATH DE number 3972158 (Why is no real title available?)
- scientific article; zbMATH DE number 3714908 (Why is no real title available?)
- scientific article; zbMATH DE number 3716792 (Why is no real title available?)
- scientific article; zbMATH DE number 3735115 (Why is no real title available?)
- scientific article; zbMATH DE number 3748393 (Why is no real title available?)
- scientific article; zbMATH DE number 3572138 (Why is no real title available?)
- scientific article; zbMATH DE number 3237829 (Why is no real title available?)
- scientific article; zbMATH DE number 3291134 (Why is no real title available?)
- scientific article; zbMATH DE number 3363520 (Why is no real title available?)
- A Weaker Precondition for Loops
- A proof rule for fair termination of guarded commands
- Adequate proof principles for invariance and liveness properties of concurrent programs
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Countable nondeterminism and random assignment
- Fair termination revisited - with delay
- Fairness and related properties in transition systems - a temporal logic to deal with fairness
- Infinite trees, markings, and well-foundedness
- On verifying that a concurrent program satisfies a nondeterministic specification
- Programming as a Discipline of Mathematical Nature
- Proof rules and transformations dealing with fairness
- Propositional dynamic logic of looping and converse is elementarily decidable
- Propositional dynamic logic of nonregular programs
- Proving Liveness Properties of Concurrent Programs
- Temporal logic can be more expressive
- Ten Years of Hoare's Logic: A Survey—Part I
- Ten years of Hoare's logic: A survey. II: Nondeterminism
- The complementation problem for Büchi automata with applications to temporal logic
- The complexity of propositional linear temporal logics
- The temporal semantics of concurrent programs
- Theories of automata on \(\omega\)-tapes: a simplified approach
- Verifying temporal properties without temporal logic
Cited in
(41)- A general notion of uniform strategies
- 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
- Automata-based verification of programs with tree updates
- Robin Milner 1934--2010
- Infinite trees, markings, and well-foundedness
- On the complexity of verifying concurrent transition systems
- Realizability of Concurrent Recursive Programs
- Recognizing safety and liveness
- Liveness-Preserving Atomicity Abstraction
- Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach
- scientific article; zbMATH DE number 1406236 (Why is no real title available?)
- Computability and realizability for interactive computations
- Automated Verification of Concurrent Search Structures
- Liminf progress measures
- Verification of sequential and concurrent programs
- Automata for true concurrency properties
- Parameterized Verification of Communicating Automata under Context Bounds
- Formal verification of language-based concurrent noninterference
- Quantum temporal logic and reachability problems of matrix semigroups
- 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
- scientific article; zbMATH DE number 734956 (Why is no real title available?)
- 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
- Realizability of concurrent recursive programs
- 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
- Inference of ranking functions for proving temporal properties by abstract interpretation
- Verifying a scheduling protocol of safety-critical systems
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)
