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. Keywords: Rely-Guarantee, Concurrency, CEGAR

Cite this paper

@inproceedings{le2020relyguarantee,
  author    = {Le, Xuan-Bach and Sanán, David and Sun, Jun and Lin, Shang-Wei},
  title     = {Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications},
  booktitle = {Proceedings of the 25th International Conference on Engineering of Complex Computer Systems (ICECCS 2020)},
  pages     = {43--52},
  publisher = {IEEE},
  year      = {2020},
  doi       = {10.1109/ICECCS51672.2020.00013}
}