Publication Type
Conference Proceeding Article
Version
acceptedVersion
Publication Date
7-2018
Abstract
Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoning for concurrent programs with shared variables. Our framework models concurrent programs as succinct automata and supports the verification of multiple important properties. Safety verification and simulations of succinct automata are parallel compositional, and safety properties of succinct automata are preserved under refinements. We generate succinct automata from infinite state concurrent programs in an automated manner. Furthermore, we propose the first automated approach to checking rely-guarantee based simulations between infinite state concurrent programs. We have prototyped our algorithms and applied our tool to the verification of multiple refinements.
Discipline
Computer Engineering | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 22nd International Symposium on Formal Methods, Oxford, UK, 2018 July 15-17
Volume
10951
First Page
523
Last Page
542
ISBN
978-3-319-95581-0
Identifier
10.1007/978-3-319-95582-7_31
City or Country
Oxford, UK
Citation
ZHANG, Fuyuan; ZHAO, Yongwang; SANAN, David; LIU, Yang; TIU, Alwen; LIN, Shang-Wei; and SUN, Jun.
Compositional reasoning for shared-variable concurrent programs. (2018). Proceedings of the 22nd International Symposium on Formal Methods, Oxford, UK, 2018 July 15-17. 10951, 523-542.
Available at: https://ink.library.smu.edu.sg/sis_research/4649
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.1007/978-3-319-95582-7_31