Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

3-2020

Abstract

Rely-Guarantee is a comprehensive technique that supports compositional reasoning for concurrent programs. However, specifications of the Rely condition - environment interference, and Guarantee condition - local transformation of thread state - are challenging to establish. Thus the construction of these conditions becomes bottleneck in automating the technique. To tackle the above problem, we propose a verification framework that, based on Rely-Guarantee principles, constructs the correctness proof of concurrent program through inferring suitable Rely -Guarantee conditions automatically. Our framework first constructs a Hoare-style sequential proof for each thread and then applies abstraction refinement to elevate these proofs into concurrent ones with appropriate Rely-Guarantee relations. Experiment results demonstrate that our approach is efficient in proving the correctness of concurrent programs.

Keywords

CEGAR, Concurrency, Rely-Guarantee

Discipline

Theory and Algorithms

Research Areas

Intelligent Systems and Optimization

Publication

2020 25th International Conference on Engineering of Complex Computer Systems ICECCS: Singapore , March 4-6: Proceedings

First Page

43

Last Page

52

ISBN

9781728185583

Identifier

10.1109/ICECCS51672.2020.00013

Publisher

IEEE Computer Society

City or Country

Los Alamitos, CA

Embargo Period

5-14-2021

Copyright Owner and License

Publisher

Additional URL

https://doi.org/10.1109/ICECCS51672.2020.00013

Download

Share

COinS