Proving the Correctness of Multiprocess Programs
From MaRDI portal
Publication:4120115
DOI10.1109/TSE.1977.229904zbMath0349.68006WikidataQ56784517 ScholiaQ56784517MaRDI QIDQ4120115
Publication date: 1977
Published in: IEEE Transactions on Software Engineering (Search for Journal in Brave)
Related Items
Efficient Runtime Verification of First-Order Temporal Properties ⋮ Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems ⋮ Local Symmetry and Compositional Verification ⋮ Safety without stuttering ⋮ Implementing dataflow with threads ⋮ Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos ⋮ Introduction to Model Checking ⋮ Modeling for Verification ⋮ Compositional Reasoning ⋮ Taming Message-Passing Communication in Compositional Reasoning About Confidentiality ⋮ Last-use opacity: a strong safety property for transactional memory with prerelease support ⋮ Clock Synchronization and Estimation in Highly Dynamic Networks: An Information Theoretic Approach ⋮ Atomic semantics of nonatomic programs ⋮ Control design for nondeterministic input/output automata ⋮ Monitorable hyperproperties of nonterminating systems ⋮ Bounded variability of metric temporal logic ⋮ Model-Checking Linear-Time Properties of Quantum Systems ⋮ Fairness and communication-based semantics for session-typed languages ⋮ Unnamed Item ⋮ Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving ⋮ Model checking with fairness assumptions using PAT ⋮ Modelling mutual exclusion in a process algebra with time-outs ⋮ On monitoring linear temporal properties ⋮ Deciding safety and liveness in TPTL ⋮ Vector Control Lyapunov and Barrier Functions for Safe Stabilization of Interconnected Systems ⋮ Quantitative safety and liveness ⋮ Just testing ⋮ The temporal semantics of concurrent programs ⋮ HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties ⋮ On the limits of refinement-testing for model-checking CSP ⋮ A predicate transformer for progress ⋮ Coalgebraic semantics of modal logics: an overview ⋮ Inference of \(\omega\)-languages from prefixes. ⋮ LTL is closed under topological closure ⋮ Linear temporal logic symbolic model checking ⋮ Which security policies are enforceable by runtime monitors? A survey ⋮ The mailbox problem ⋮ An abstract interpretation-based model for safety semantics ⋮ Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs ⋮ Probabilistic Lipschitz analysis of neural networks ⋮ Adequacy-preserving transformations of COSY path programs ⋮ The Automatic Detection of Token Structures and Invariants Using SAT Checking ⋮ A complete characterization of deterministic regular liveness properties ⋮ Conditions of contracts for separating responsibilities in heterogeneous systems ⋮ Inference of ranking functions for proving temporal properties by abstract interpretation ⋮ Sooner is safer than later ⋮ Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions ⋮ Execution monitoring enforcement under memory-limitation constraints ⋮ Loop invariants ⋮ Runtime enforcement monitors: Composition, synthesis, and enforcement abilities ⋮ The weakest failure detector for eventual consistency ⋮ Turing machines, transition systems, and interaction ⋮ Ensuring liveness properties of distributed systems: open problems ⋮ Formal specification and analysis of production systems ⋮ Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory ⋮ Unnamed Item ⋮ Fifty years of Hoare's logic ⋮ Model checking of linear-time properties in multi-valued systems ⋮ Robustness in Interaction Systems ⋮ Mitigating Multi-target Attacks in Hash-Based Signatures ⋮ Characterization of temporal property classes ⋮ Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems ⋮ Automatically verifying temporal properties of pointer programs with cyclic proof ⋮ A proof system for disjoint parallel quantum programs ⋮ Integration of formal proof into unified assurance cases with Isabelle/SACM ⋮ On the refinement of liveness properties of distributed systems ⋮ The F-Snapshot Problem ⋮ Livelocks in parallel programs ⋮ Programming interfaces and basic topology ⋮ Razumikhin and Krasovskii approaches for safe stabilization ⋮ Enforcing Non-safety Security Policies with Program Monitors ⋮ Defining liveness ⋮ The existence of refinement mappings ⋮ Safety and liveness of \(\omega\)-context-free languages ⋮ Two-process synchronization
