Reduction
From MaRDI portal
Cited in
(52)- Synthesizing precise and useful commutativity conditions
- Accelerating the computation of dead and concurrent places using reductions
- A mechanized refinement proof of the Chase-Lev deque using a proof system
- Structural reductions and stutter sensitive properties
- Strict linearizability and abstract atomicity
- Proving Isolation Properties for Software Transactional Memory
- Simulation Refinement for Concurrency Verification
- Simulation refinement for concurrency verification
- Commutation properties and generating sets characterize slices of various synchronization primitives
- Symbolic and structural model-checking
- Software Verification of Hyperproperties Beyond k-Safety
- scientific article; zbMATH DE number 7561456 (Why is no real title available?)
- Proving the correctness of client/server software
- Flashix: modular verification of a concurrent and crash-safe flash file system
- Guessing the buffer bound for k-synchronizability
- Synchronizing the asynchronous
- On the k-synchronizability of systems
- Trace-based derivation of a scalable lock-free stack algorithm
- Checking robustness between weak transactional consistency models
- A reduction theorem for randomized distributed algorithms under weak adversaries
- Decomposing data structure commutativity proofs with \(mn\)-differencing
- Optimistic synchronization-based state-space reduction
- Presynthesis of bounded choice-free or fork-attribution nets
- Dynamic reductions for model checking concurrent software
- Constraining interference in an object-based design method
- Fifty years of Hoare's logic
- Homomorphisms between models of parallel computation
- Structural reductions revisited
- On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- Using refinement calculus techniques to prove linearizability
- Guessing the Buffer Bound for k-Synchronizability
- Livelocks in parallel programs
- Program refinement in fair transition systems
- Refinement algebra for probabilistic programs
- LTL under reductions with weaker conditions than stutter invariance
- Choose your proofs: commutativity and symmetry for smarter reasoning
- A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking
- A theorem on atomicity in distributed algorithms
- A sound and complete proof technique for linearizability of concurrent data structures
- Security monitor inlining and certification for multithreaded Java
- Modular verification of multithreaded programs
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- Procedures and atomicity refinement
- Simulation, reduction and preservation of correctness properties of parallel systems
- \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
- Composing leads-to properties
- Commutativity for concurrent program termination proofs
- On reduction of asynchronous systems
- Predicate abstraction for hyperliveness verification
- Transformational semantics for concurrent programs
- The Complexity of Predicting Atomicity Violations
This page was built for publication: Reduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4077431)
