Incremental Verification of Concurrent Programs through Refinement Constraint Adaptation
Programs evolve continuously throughout their life cycles. Verifying each version from scratch is usually impractical, especially for concurrent programs. Designing efficient incremental verification techniques for concurrent programs is highly desired. We focus on the abstraction refinement technique for concurrent program verification. When a program is modified, those refinement constraints generated in those verifications of former versions are adapted to the new program to avoid redundant analysis. We propose a kernel source based refinement constraint adaptation approach for the scheduling constraint based abstraction refinement method, one of the most efficient abstraction refinement methods for concurrent program verification. Our method supports all kinds of program modifications, and generates adapted refinement constraints according to the modifications. Evaluation on the benchmarks from SV-COMP 2024 show promising results of our method. Most of the refinement constraints generated in the verification of previous versions can be adapted to the modified program in our experiments. Compared with verifying the modified program from scratch, our incremental verification method can achieve an order of magnitude speedup for those complex programs.
Fri 27 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:15 | |||
11:00 25mTalk | Bridging the Gaps Between Graph Neural Networks and Data-Flow Analysis: The Closer, the Better Research Papers Qingchen Yu Zhejiang University, Xin Liu Lanzhou University, Qingguo Zhou Lanzhou University, Chunming Wu Zhejiang University DOI | ||
11:25 25mTalk | Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference Research Papers Weining Cao Nanjing University, China, Guangyuan Wu Nanjing University, China, Tangzhi Xu Nanjing University, China, Yuan Yao Nanjing University, Hengfeng Wei State Key Laboratory for Novel Software Technology, Nanjing University, Taolue Chen Birkbeck, University of London, Xiaoxing Ma Nanjing University DOI | ||
11:50 25mTalk | Incremental Verification of Concurrent Programs through Refinement Constraint Adaptation Research Papers Liangze Yin National University of Defense Technology, Yiwei Li , Kun Chen National University of Defense Technology, Wei Dong National University of Defense Technology, Ji Wang National University of Defense Technology DOI | ||
Cosmos 3B is the second room in the Cosmos 3 wing.
When facing the main Cosmos Hall, access to the Cosmos 3 wing is on the left, close to the stairs. The area is accessed through a large door with the number “3”, which will stay open during the event.