Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications

Abstract

Rely-Guarantee is a comprehensive technique that supports compositional reasoning for concurrent programs. However, specifying the Rely condition—environment interference—and the Guarantee condition—local transformation of thread state—remains challenging, making their construction a major bottleneck in automation. To address this problem, we propose a verification framework that constructs correctness proofs for concurrent programs by automatically inferring suitable Rely-Guarantee conditions. Our framework first builds a Hoare-style sequential proof for each thread, and then applies abstraction refinement to lift these proofs into concurrent ones with appropriate Rely-Guarantee relations. Experimental results demonstrate that our approach efficiently proves the correctness of multi-threaded programs.