Proving Liveness Properties of Concurrent Programs
From MaRDI portal
Cited in
(79)- Processes with local and global liveness requirements
- An approach to automating the verification of compact parallel coordination programs. I
- Specification-oriented semantics for communicating processes
- Defining liveness
- On powerdomains and modality
- Sometime = always + recursion always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
- Verification of multiprocess probabilistic protocols
- The complementation problem for Büchi automata with applications to temporal logic
- Specification and verification of database dynamics
- Proving entailment between conceptual state specifications
- On the analysis of cooperation and antagonism in networks of communicating processes
- A shared memory algorithm and proof for the generalized alternative construct in CSP
- On conceptual model specification and verification
- Fairness and the axioms of control predicates
- Deadlock and fairness in morphisms of transition systems
- Semantics and verification of monitors and systems of monitors and processes
- Appraising fairness in languages for distributed programming
- The power of temporal proofs
- Problems concerning fairness and temporal logic for conflict-free Petri nets
- Concurrent systems and inevitability
- Correctness of concurrent processes
- Completing the temporal picture
- Weakest preconditions for progress
- The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\)
- Specifying modules to satisfy interfaces: A state transition system approach
- Axiomatic treatment of processes with shared variables revisited
- Verification of distributed programs using representative interleaving sequences
- Safety, liveness and fairness in temporal logic
- A logic for reasoning about time and reliability
- Formalizing process algebraic verifications in the calculus of constructions
- A methodology for designing proof rules for fair parallel programs
- Finite automata on timed \(\omega\)-trees
- On relative and probabilistic finite counterability
- Using partial orders for the efficient verification of deadlock freedom and safety properties
- Weak and strong fairness in CCS
- A formal model of atomicity in asynchronous systems
- Distributed automata in an assumption-commitment framework
- On fairness notions in distributed systems. I: A characterization of implementability
- Compositional verification of real-time systems with explicit clock temporal logic
- An axiomatic approach to existence and liveness for differential equations
- Why there is no general solution to the problem of software verification
- Using session types for reasoning about boundedness in the \(\pi\)-calculus
- Verification of concurrent programs: The automata-theoretic framework
- Proof-based verification approaches for dynamic properties: application to the information system domain
- Deadness and how to disprove liveness in hybrid dynamical systems
- An abstract interpretation-based model for safety semantics
- Fairness, resources, and separation
- The Birth of Model Checking
- Méthode axiomatique sur les propriétés de fatalité des programmes parallèles
- Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems
- Assurance of dynamic adaptation in distributed systems
- Removing irrelevant information in temporal resolution proofs
- Verification of correctness of parallel algorithms in practice
- Linear temporal logic symbolic model checking
- Analysing mutual exclusion using process algebra with signals
- Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types
- On mechanizing proofs within a complete proof system for Unity
- Efficient detection of a class of stable properties
- Fast timing-based algorithms
- Knowledge-based programs
- Automatic verification for a class of distributed systems
- A note on knowledge-based programs and specifications
- Direct formal verification of liveness properties in continuous and hybrid dynamical systems
- Retracing CSP
- Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement
- Modelling and verification of Distributed Algorithms
- Automatic temporal verification of buffer systems
- Using partial orders for the efficient verification of deadlock freedom and safety properties
- An axiomatic approach to liveness for differential equations
- Automated temporal reasoning about reactive systems
- An automata-theoretic approach to linear temporal logic
- Fair termination of multiparty sessions
- Attempting guards in parallel: A data flow approach to execute generalized guarded commands
- Inference systems with corules for fair subtyping and liveness properties of binary session types
- On the refinement of liveness properties of distributed systems
- A fair calculus of communicating systems
- A generalized nexttime operator in temporal logic
- A semantics for concurrent separation logic
- Branching versus linear logics yet again
This page was built for publication: Proving Liveness Properties of Concurrent Programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3942371)
