2024/05/09 by Larissa Meinicke, Ian J. Hayes, Meinicke, Larissa A. +3
Computer Science · Engineering · #Advanced Algebra and Logic #D.1.3 #F.3.1 #FOS: Computer and information sciences #Fault Detection and Control Systems #Logic in Computer Science (cs.LO) #Software Engineering (cs.SE) #Stability and Control of Uncertain Systems
paper · pdf · doi:10.48550/arxiv.2405.05546
openalex publication_date 2024/05/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Specifications of significant systems can be made short and perspicuous by using abstract data types; data reification can provide a clear, stepwise, development history of programs that use more efficient concrete representations. Data reification (or "refinement") techniques for sequential programs are well established. This paper applies these ideas to concurrency, in particular, an algebraic theory supporting rely-guarantee reasoning about concurrency. A concurrent version of the Galler-Fischer equivalence relation data structure is used as an example.