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
Citation
LE, Xuan-Bach; SANAN, David; SUN, Jun; and LIN, Shang-Wei.
Automatic verification of multi-threaded programs by inference of rely-guarantee specifications. (2020). 2020 25th International Conference on Engineering of Complex Computer Systems ICECCS: Singapore , March 4-6: Proceedings. 43-52.
Available at: https://ink.library.smu.edu.sg/sis_research/5939
Copyright Owner and License
Publisher
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1109/ICECCS51672.2020.00013
