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