Verification of concurrent programs: The automata-theoretic framework
An effective version of Wolper's temporal logic IPTL, recursive infinitary temporal logic (RITL) is introduced, and it is proved that the properties expressed in RITL can be captured by recursive automata on infinite trees. Three types of acceptance conditions (Wolper acceptance, Büchi acceptance, and Streett acceptance) for these automata are considered and shown to be of the same power. This enables to define effective equivalent transformations of recursive trees with complicated correctness conditions to trees with simpler ones (nondeterministic programs are naturally associated to their computational trees, which are recursive). This transformation technique is then applied to verification of concurrent and nondeterministic programs. Proof methods for two approaches to fair termination are developed: the method of explicit schedulers, and the method of helpful directions. The idea is that, given a computation tree of a program and a correctness condition, both defined via recursive automata, one constructs new automata which terminate iff the program is correct. If, for example, the correctness is formulated in RITL, we can express it in terms of recursive automata. Hence correctness is reduced to termination.
- 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
- A proof rule for fair termination of guarded commands
- A Weaker Precondition for Loops
- 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
- 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?)
- 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. II: Nondeterminism
- Ten Years of Hoare's Logic: A Survey—Part I
- 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
- Recognizing safety and liveness
- Infinite trees, markings, and well-foundedness
- Realizability of concurrent recursive programs
- Automata for true concurrency properties
- A compositional approach to CTL^* verification
- On the role of automated theorem proving in the compile-time derivation of concurrency
- Verification by augmented finitary abstraction
- On control of systems modelled as deterministic Rabin automata
- Automatic and hierarchical verification for concurrent systems
- Computability and realizability for interactive computations
- Uniform strategies, rational relations and jumping automata
- Verifying a scheduling protocol of safety-critical systems
- Bridging the gap between fair simulation and trace inclusion
- Formalization and correctness of a concurrent linear hash structure algorithm using nested transactions and I/O automata
- Verification of parameterized concurrent programs by modular reasoning about data and control
- Caper
- Liveness-Preserving Atomicity Abstraction
- Verifying Concurrent Systems with Symbolic Execution
- Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach
- Parameterized Verification of Communicating Automata under Context Bounds
- Realizability of Concurrent Recursive Programs
- scientific article; zbMATH DE number 734956 (Why is no real title available?)
- scientific article; zbMATH DE number 1406236 (Why is no real title available?)
- Automated Verification of Concurrent Search Structures
- Streett Automata Model Checking of Higher-Order Recursion Schemes
- Formal verification of language-based concurrent noninterference
- A general notion of uniform strategies
- Robin Milner 1934--2010
- Automatically verifying temporal properties of pointer programs with cyclic proof
- Verification by augmented abstraction: The automata-theoretic view
- On the complexity of verifying concurrent transition systems
- Towards a grand unification of Büchi complementation constructions
- Liminf progress measures
- Quantum temporal logic and reachability problems of matrix semigroups
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
- Inference of ranking functions for proving temporal properties by abstract interpretation
- On the refinement of liveness properties of distributed systems
- Verification of sequential and concurrent programs
- Automata-based verification of programs with tree updates
- Deductive verification of alternating systems
- Model checking duration calculus: a practical approach
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)
