Parametrized Invariance for Infinite State Processes

TL;DR

This paper introduces a novel parametrized invariance framework for verifying safety properties of infinite state concurrent programs, enabling automatic, scalable, and data-type agnostic verification using SMT solvers.

Contribution

It presents a general verification method that separates thread interaction from data manipulation, automates verification conditions, and supports complex data types with off-the-shelf SMT solvers.

Findings

Successfully verified a concurrent list implementation.

Verification conditions are finite, quantifier-free, and independent of process count.

The approach integrates with existing SMT solvers for practical verification.

Abstract

We study the uniform verification problem for infinite state processes, which consists of proving that the parallel composition of an arbitrary number of processes satisfies a temporal property. Our practical motivation is to build a general framework for the temporal verification of concurrent datatypes. The contribution of this paper is a general method for the verification of safety properties of parametrized programs that manipulate complex local and global data, including mutable state in the heap. This method is based on the separation between two concerns: (1) the interaction between executing threads---handled by novel parametrized invariance rules---,and the data being manipulated---handled by specialized decision procedures. The proof rules discharge automatically a finite collection of verification conditions (VCs), the number depending only on the size of the program description and the specification, but not on the number of processes in any given instance or on the kind of data manipulated. Moreover, all VCs are quantifier free, which eases the development of decision procedures for complex data-types on top of off-the-shelf SMT solvers. We discuss the practical verification (of shape and also functional correctness properties) of a concurrent list implementation based on the method presented in this paper. Our tool also all VCs using a decision procedure for a theory of list layouts in the heap built on top of state-of-the-art SMT solvers.