Proving the Correctness of Multiprocess Programs

Cited In (77)

Execution monitoring enforcement under memory-limitation constraints
A complete characterization of deterministic regular liveness properties
Razumikhin and Krasovskii approaches for safe stabilization
Safety without stuttering
HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
A predicate transformer for progress
Deciding safety and liveness in TPTL
Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions
Turing machines, transition systems, and interaction
Model checking of linear-time properties in multi-valued systems
A proof system for disjoint parallel quantum programs
An abstract interpretation-based model for safety semantics
Formal specification and analysis of production systems
Clock synchronization and estimation in highly dynamic networks: an information theoretic approach
Model-checking linear-time properties of quantum systems
The existence of refinement mappings
Defining liveness
Atomic semantics of nonatomic programs
Conditions of contracts for separating responsibilities in heterogeneous systems
The weakest failure detector for eventual consistency
Probabilistic Lipschitz analysis of neural networks
Direct formal verification of liveness properties in continuous and hybrid dynamical systems
Fifty years of Hoare's logic
Robustness in Interaction Systems
Two-process synchronization
Mitigating multi-target attacks in hash-based signatures
The temporal semantics of concurrent programs
Coalgebraic semantics of modal logics: an overview
Loop invariants: analysis, classification, and examples
Just testing
Static analysis of run-time errors in embedded critical parallel C programs
Control design for nondeterministic input/output automata
Title not available (Why is that?)
Linear temporal logic symbolic model checking
Which security policies are enforceable by runtime monitors? A survey
Runtime enforcement monitors: Composition, synthesis, and enforcement abilities
Fairness and communication-based semantics for session-typed languages
Monitorable hyperproperties of nonterminating systems
On the refinement of liveness properties of distributed systems
Efficient Runtime Verification of First-Order Temporal Properties
Adequacy-preserving transformations of COSY path programs
Introduction to model checking
Integration of formal proof into unified assurance cases with Isabelle/SACM
Inference of \(\omega\)-languages from prefixes.
Automatically verifying temporal properties of pointer programs with cyclic proof
Title not available (Why is that?)
Bounded variability of metric temporal logic
Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
On monitoring linear temporal properties
Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
Model checking with fairness assumptions using PAT
The mailbox problem
Enforcing non-safety security policies with program monitors
Characterization of temporal property classes
Ensuring liveness properties of distributed systems: open problems
Last-use opacity: a strong safety property for transactional memory with prerelease support
Implementing dataflow with threads
The automatic detection of token structures and invariants using SAT checking
On the limits of refinement-testing for model-checking CSP
Compositional reasoning
Safety and liveness of \(\omega\)-context-free languages
Sooner is safer than later
Inference of ranking functions for proving temporal properties by abstract interpretation
LTL is closed under topological closure
Modeling for Verification
Modelling mutual exclusion in a process algebra with time-outs
SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks
Vector Control Lyapunov and Barrier Functions for Safe Stabilization of Interconnected Systems
Livelocks in parallel programs
Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
Quantitative safety and liveness
Programming interfaces and basic topology
The F-Snapshot Problem
Taming Message-Passing Communication in Compositional Reasoning About Confidentiality
Local symmetry and compositional verification
Aneris: a mechanised logic for modular reasoning about distributed systems
Refining the Safety-Liveness Classification of Temporal Properties According to Realizability

This page was built for publication: Proving the Correctness of Multiprocess Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4120115)