Compositional Reasoning for Shared-variable Concurrent Programs

TL;DR

This paper introduces an automated framework for compositional reasoning in shared-variable concurrent programs, enabling scalable verification of safety properties through succinct automata modeling and automated simulations.

Contribution

It presents the first automated approach to verify rely-guarantee simulations and models concurrent programs as succinct automata for scalable safety verification.

Findings

Automated generation of succinct automata from infinite state programs.

Parallel compositional safety verification of succinct automata.

Successful application to multiple program refinements.

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.