2014/08/05 by Duc-Hiep Chu, Chu, Duc-Hiep, Joxan Jaffar +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #Software Reliability and Analysis Research #Software Testing and Debugging Techniques #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.1408.0957
arxiv created 2014/08/05 · openalex publication_date 2014/08/05 · arxiv updated 2014/08/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We address the problem of reasoning about interleavings in safety verification of concurrent programs. In the literature, there are two prominent techniques for pruning the search space. First, there are well-investigated trace-based methods, collectively known as "Partial Order Reduction (POR)", which operate by weakening the concept of a trace by abstracting the total order of its transitions into a partial order. Second, there is state-based interpolation where a collection of formulas can be generalized by taking into account the property to be verified. Our main contribution is a framework that synergistically combines POR with state interpolation so that the sum is more than its parts.