Proving the Correctness of Multiprocess Programs

Cited in

(82)

Execution monitoring enforcement under memory-limitation constraints
A complete characterization of deterministic regular liveness properties
Safety without stuttering
Razumikhin and Krasovskii approaches for safe stabilization
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
HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
Turing machines, transition systems, and interaction
Model checking of linear-time properties in multi-valued systems
Safety and liveness of quantitative automata
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
LTL is closed under topological closure
Model-checking linear-time properties of quantum systems
The existence of refinement mappings
Defining liveness
Safety and liveness of quantitative properties and automata
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
Composition: a way to make proofs harder
The temporal semantics of concurrent programs
Mitigating multi-target attacks in hash-based signatures
Modeling for Verification
Coalgebraic semantics of modal logics: an overview
Modelling mutual exclusion in a process algebra with time-outs
Loop invariants: analysis, classification, and examples
SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks
Vector Control Lyapunov and Barrier Functions for Safe Stabilization of Interconnected Systems
Just testing
Static analysis of run-time errors in embedded critical parallel C programs
Control design for nondeterministic input/output automata
Linear temporal logic symbolic model checking
Which security policies are enforceable by runtime monitors? A survey
Livelocks in parallel programs
Runtime enforcement monitors: Composition, synthesis, and enforcement abilities
scientific article; zbMATH DE number 7350777 (Why is no real title available?)
Fairness and communication-based semantics for session-typed languages
On the refinement of liveness properties of distributed systems
Monitorable hyperproperties of nonterminating systems
Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
Programming interfaces and basic topology
Quantitative safety and liveness
Adequacy-preserving transformations of COSY path programs
The F-Snapshot Problem
Efficient Runtime Verification of First-Order Temporal Properties
Introduction to model checking
Integration of formal proof into unified assurance cases with Isabelle/SACM
Inference of -languages from prefixes.
Automatically verifying temporal properties of pointer programs with cyclic proof
scientific article; zbMATH DE number 7566044 (Why is no real title available?)
Taming Message-Passing Communication in Compositional Reasoning About Confidentiality
Bounded variability of metric temporal logic
Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
Local symmetry and compositional verification
Verification of time-bounded multiset rewriting properties
The mailbox problem
Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
Model checking with fairness assumptions using PAT
On monitoring linear temporal properties
Ensuring liveness properties of distributed systems: open problems
Enforcing non-safety security policies with program monitors
Last-use opacity: a strong safety property for transactional memory with prerelease support
Characterization of temporal property classes
Implementing dataflow with threads
The automatic detection of token structures and invariants using SAT checking
Aneris: a mechanised logic for modular reasoning about distributed systems
On the limits of refinement-testing for model-checking CSP
Safety and liveness of \(\omega\)-context-free languages
Compositional reasoning
Sooner is safer than later
Refining the Safety-Liveness Classification of Temporal Properties According to Realizability
Inference of ranking functions for proving temporal properties by abstract interpretation
Semantics for linear-time temporal logic with finite observations

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)