Proving Liveness Properties of Concurrent Programs
From MaRDI portal
Publication:3942371
DOI10.1145/357172.357178zbMath0483.68013OpenAlexW2166656159MaRDI QIDQ3942371
Publication date: 1982
Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/357172.357178
fairnesssynchronizationtemporal logicconcurrent programmingprogram verificationproof of correctnesssemantics of programming languagesmultiprocessing
Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)
Related Items
Verification of multiprocess probabilistic protocols, Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types, The complementation problem for Büchi automata with applications to temporal logic, Deadness and how to disprove liveness in hybrid dynamical systems, Safety, liveness and fairness in temporal logic, A logic for reasoning about time and reliability, Specification and verification of database dynamics, Proving entailment between conceptual state specifications, Fairness, Resources, and Separation, 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, Formalizing process algebraic verifications in the calculus of constructions, Why there is no general solution to the problem of software 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, A methodology for designing proof rules for fair parallel programs, Compositional verification of real-time systems with explicit clock temporal logic, Concurrent systems and inevitability, A semantics for concurrent separation logic, On mechanizing proofs within a complete proof system for Unity, Méthode axiomatique sur les propriétés de fatalité des programmes parallèles, Finite automata on timed \(\omega\)-trees, Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems, Modelling and verification of Distributed Algorithms, The Birth of Model Checking, Assurance of dynamic adaptation in distributed systems, Branching versus linear logics yet again, Verification of Correctness of Parallel Algorithms in Practice, Unnamed Item, Using session types for reasoning about boundedness in the \(\pi\)-calculus, Linear temporal logic symbolic model checking, 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, Correctness of concurrent processes, Completing the temporal picture, An abstract interpretation-based model for safety semantics, An axiomatic approach to existence and liveness for differential equations, Weakest preconditions for progress, On relative and probabilistic finite counterability, 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, 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, Verification of concurrent programs: The automata-theoretic framework, Removing irrelevant information in temporal resolution proofs, Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems, Using partial orders for the efficient verification of deadlock freedom and safety properties, Processes with local and global liveness requirements, On the refinement of liveness properties of distributed systems, Weak and strong fairness in CCS, A formal model of atomicity in asynchronous systems, Distributed automata in an assumption-commitment framework, A fair calculus of communicating systems, An approach to automating the verification of compact parallel coordination programs. I, On fairness notions in distributed systems. I: A characterization of implementability, Specification-oriented semantics for communicating processes, A generalized nexttime operator in temporal logic, Retracing CSP, Defining liveness, On powerdomains and modality, Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs, Proof-based verification approaches for dynamic properties: application to the information system domain
