Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications
17/03/2021
Speaker
Xuan-Bach Le (NTU)
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 programs 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.
Speaker Bio
Xuan-Bach Le received his PhD from NUS in 2018. For his PhD studies, he has worked extensively on the tree share structure proposed by Dockins et al. in which he applied it to reason about resource ownership in separation logic. In general, his research interests are formal methods and decision procedures that can support program verification. Since his PhD, he has worked as postdoc at Oxfords and then NTU. He now works on developing verification frameworks forconcurrent programs and quantum programs.