Preserving hyperproperties of programs using primitives with consensus number 2
From MaRDI portal
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites work
- A completeness theorem for a class of synchronization objects
- Abstraction for concurrent objects
- Atomic snapshots of shared memory
- Common2 extended to stacks and unbounded concurrency
- Forward and backward simulations. I. Untimed Systems
- From bounded to unbounded concurrency objects and back
- scientific article; zbMATH DE number 795590 (Why is no real title available?)
- scientific article; zbMATH DE number 7774258 (Why is no real title available?)
- scientific article; zbMATH DE number 7832769 (Why is no real title available?)
- scientific article; zbMATH DE number 7832770 (Why is no real title available?)
- Linearizable implementations do not suffice for randomized distributed computation
- MAX registers, counters, and monotone circuits
- Model checking algorithms for hyperproperties (invited paper)
- Monitoring hyperproperties
- Preserving Secrecy Under Refinement
- Putting strong linearizability in context: preserving hyperproperties in programs that use concurrent objects
- Quantitative relaxation of concurrent data structures
- Randomized protocols for asynchronous consensus
- Set consensus using arbitrary objects (preliminary version)
- Set-linearizable implementations from read/write operations: sets, fetch \& increment, stacks and queues with multiplicity
- Simple relational correctness proofs for static analyses and program transformations
- Strong linearizability using primitives with consensus number 2
- Strongly Linearizable Implementations of Snapshots and Other Types
- Strongly linearizable implementations, possibilities and impossibilities
- Synthesis from hyperproperties
- The hierarchy of hyperlogics
- The Instancy of Snapshots and Commuting Objects
- Tractable refinement checking for concurrent objects
- Wait-freedom is harder than lock-freedom under strong linearizability
- Weak progressive forward simulation is necessary and sufficient for strong observational refinement
This page was built for publication: Preserving hyperproperties of programs using primitives with consensus number 2
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6939171)
