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

Additional URL

https://doi.org/10.1007/978-3-319-95582-7_31

Share

COinS