2025/12/06 by Hayes, Ian J., Meinicke, Larissa A., Jones, Cliff B.
Computer Science · #D.1.3 #F.3.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Engineering (cs.SE)
paper · doi:10.48550/arxiv.2512.06242
openalex publication_date 2025/12/06 · openalex created_date 2025/12/10 · openalex updated_date 2026/07/28
The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. We make use of the rely-guarantee approach to concurrency that facilitates reasoning about interference from concurrent threads in a compositional manner. Recursive programs can be defined as fixed points over a lattice of commands and hence we develop laws for reasoning about fixed points. Loops can be defined in terms of fixed points and hence the laws for recursion can be applied to develop laws for loops. Unlike many approaches to concurrency, we do not assume that expression evaluation is atomic.