Reduction

DOI10.1145/361227.361234zbMath0316.68015OpenAlexW2072062729MaRDI QIDQ4077431

Richard J. Lipton

Publication date: 1975

Published in: Communications of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/361227.361234

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Algorithms in computer science (68W99)

Related Items (48)

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ Accelerating the computation of dead and concurrent places using reductions ⋮ A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking ⋮ Constraining interference in an object-based design method ⋮ Procedures and atomicity refinement ⋮ Optimistic synchronization-based state-space reduction ⋮ LTL under reductions with weaker conditions than stutter invariance ⋮ A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Structural Reductions Revisited ⋮ Guessing the Buffer Bound for k-Synchronizability ⋮ Transformational semantics for concurrent programs ⋮ Using refinement calculus techniques to prove linearizability ⋮ \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms ⋮ Dynamic Reductions for Model Checking Concurrent Software ⋮ On the \(k\)-synchronizability of systems ⋮ Unnamed Item ⋮ Synthesizing precise and useful commutativity conditions ⋮ A theorem on atomicity in distributed algorithms ⋮ A mechanized refinement proof of the Chase-Lev deque using a proof system ⋮ Proving Isolation Properties for Software Transactional Memory ⋮ Checking robustness between weak transactional consistency models ⋮ Decomposing data structure commutativity proofs with \(mn\)-differencing ⋮ A reduction theorem for randomized distributed algorithms under weak adversaries ⋮ Simulation Refinement for Concurrency Verification ⋮ Simulation refinement for concurrency verification ⋮ Security monitor inlining and certification for multithreaded Java ⋮ Modular verification of multithreaded programs ⋮ Refinement algebra for probabilistic programs ⋮ Unnamed Item ⋮ Fifty years of Hoare's logic ⋮ On reduction of asynchronous systems ⋮ On the completeness of bounded model checking for threshold-based distributed algorithms: reachability ⋮ The Complexity of Predicting Atomicity Violations ⋮ Commutation properties and generating sets characterize slices of various synchronization primitives ⋮ Unnamed Item ⋮ Presynthesis of bounded choice-free or fork-attribution nets ⋮ Trace-based derivation of a scalable lock-free stack algorithm ⋮ Proving the correctness of client/server software ⋮ Composing leads-to properties ⋮ Homomorphisms between models of parallel computation ⋮ Livelocks in parallel programs ⋮ Simulation, reduction and preservation of correctness properties of parallel systems ⋮ Strict Linearizability and Abstract Atomicity ⋮ Symbolic and Structural Model-Checking ⋮ Program refinement in fair transition systems ⋮ On the combination of polyhedral abstraction and SMT-based model checking for Petri nets ⋮ Flashix: modular verification of a concurrent and crash-safe flash file system ⋮ Guessing the buffer bound for k-synchronizability

This page was built for publication: Reduction