@inproceedings{9093daa6197c4ad9b3227a9d51142647,
title = "Compositional reasoning for shared-variable concurrent programs",
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.",
author = "Fuyuan Zhang and Yongwang Zhao and David San{\'a}n and Yang Liu and Alwen Tiu and Lin, {Shang Wei} and Jun Sun",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG, part of Springer Nature 2018.; 22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 15-07-2018 Through 17-07-2018",
year = "2018",
doi = "10.1007/978-3-319-95582-7_31",
language = "English",
isbn = "9783319955810",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "523--541",
editor = "Klaus Havelund and Bill Roscoe and {de Vink}, Erik and Jan Peleska",
booktitle = "Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",
address = "Germany",
}