Verifying Visibility-Based Weak Consistency

DOI10.1007/978-3-030-44914-8_11OpenAlexW3022621909MaRDI QIDQ5041095

Constantin Enea, Michael Emmi, Dejan Jovanović, Siddharth Krishna

Publication date: 13 October 2022

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1911.01508

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• GRASShopper
• Unnamed Item

Cites Work

• The existence of refinement mappings
• On reducing linearizability to state reachability
• \textsc{Poling}: SMT aided linearizability proofs
• Forward and backward simulations. I. Untimed Systems
• Proving linearizability using forward simulations
• Automated Verification of Practical Garbage Collectors
• E-matching for Fun and Profit
• Quantitative relaxation of concurrent data structures
• Proving Linearizability Using Partial Orders
• Dafny: An Automatic Program Verifier for Functional Correctness
• On abstraction and compositionality for weak-memory linearisability
• Owicki-Gries Reasoning for Weak Memory Models
• Shape-Value Abstraction for Verifying Linearizability
• RGSep Action Inference
• Verifying properties of parallel programs
• Local linearizability for concurrent container-type data structures
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Aspect-oriented linearizability proofs
• CONCUR 2004 - Concurrency Theory
• An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
• Automated Deduction – CADE-20
• Replicated data types
• Comparison Under Abstraction for Verifying Linearizability

This page was built for publication: Verifying Visibility-Based Weak Consistency