Decomposing data structure commutativity proofs with \(mn\)-differencing

DOI10.1007/978-3-030-67067-2_5zbMath1472.68090OpenAlexW3119735966MaRDI QIDQ2234060

Eric Koskinen, Kshitij Bansal

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-67067-2_5

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• Relational separation logic
• On reducing linearizability to state reachability
• Learning commutativity specifications
• Modular product programs
• Automatic generation of precise and useful commutativity conditions
• Reduction
• ReLoC
• Coarse-grained transactions
• Static Analysis
• Layered concurrent programs
• Automated hypersafety verification

This page was built for publication: Decomposing data structure commutativity proofs with \(mn\)-differencing