Synthesizing precise and useful commutativity conditions

DOI10.1007/S10817-020-09573-WMaRDI QIDQ2208295zbMATH OpenOpenAlexFDO

Authors Kshitij Bansal, Eric Koskinen, Omer Tripp

Publication date 2 November 2020

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-020-09573-w

zbMATH Keywords

abstraction refinementcommutativitysynthesis

Mathematics Subject Classification ID

Data structures (68P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Automatic generation of precise and useful commutativity conditions
• Decomposing data structure commutativity proofs with \(mn\)-differencing
• On the Complexity of Commutativity Analysis
• Learning commutativity specifications
• Commutativity and its role in the processing of linear recursion

Cites work

• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• Abstraction-guided synthesis of synchronization
• Adding concurrency to smart contracts
• Automatic generation of precise and useful commutativity conditions
• Coarse-grained transactions
• Commutativity-based concurrency control for abstract data types
• scientific article; zbMATH DE number 1722942 (Why is no real title available?)
• Learning commutativity specifications
• Making prophecies with decision predicates
• Peephole Partial Order Reduction
• Reduction
• Specification of Abstract Data Types in Modula
• The existence of refinement mappings

Cited in

(5)

• Learning commutativity specifications
• Decomposing data structure commutativity proofs with \(mn\)-differencing
• Automatic generation of precise and useful commutativity conditions
• On the Complexity of Commutativity Analysis
• On the complexity of commutativity analysis

Describes a project that uses

Uses Software

• Servois
• Solidity
• Spec#
• CVC4
• GitHub

This page was built for publication: Synthesizing precise and useful commutativity conditions

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