Decomposing data structure commutativity proofs with mn-differencing

DOI10.1007/978-3-030-67067-2_5MaRDI QIDQ2234060zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Synthesizing precise and useful commutativity conditions
• Automatic generation of precise and useful commutativity conditions
• On the Complexity of Commutativity Analysis
• A constructive approach for proving data structures' linearizability
• Learning commutativity specifications

Cites work

• Automated hypersafety verification
• Automatic generation of precise and useful commutativity conditions
• Coarse-grained transactions
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 1903378 (Why is no real title available?)
• Layered concurrent programs
• Learning commutativity specifications
• Modular product programs
• Reduction
• Relational logic with framing and hypotheses
• Relational separation logic
• ReLoC: a mechanised relational logic for fine-grained concurrency
• Static Analysis
• The existence of refinement mappings

Cited in

(4)

• Synthesizing precise and useful commutativity conditions
• Automatic generation of precise and useful commutativity conditions
• On the Complexity of Commutativity Analysis
• On the complexity of commutativity analysis

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2234060)