Synthesizing precise and useful commutativity conditions

DOI10.1007/s10817-020-09573-wzbMath1468.68079OpenAlexW3082023611MaRDI QIDQ2208295

Omer Tripp, Eric Koskinen, Kshitij Bansal

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

synthesiscommutativityabstraction refinement

Mathematics Subject Classification ID

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

Uses Software

• Spec#
• CVC4
• GitHub
• Servois
• Solidity

Cites Work

• Unnamed Item
• The existence of refinement mappings
• Learning commutativity specifications
• Adding concurrency to smart contracts
• Automatic generation of precise and useful commutativity conditions
• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• Commutativity-based concurrency control for abstract data types
• Specification of Abstract Data Types in Modula
• Reduction
• Coarse-grained transactions
• Abstraction-guided synthesis of synchronization
• Making prophecies with decision predicates
• Peephole Partial Order Reduction

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