Parametrized Verification Diagrams

Abstract

We study the uniform verification problem for infinite state processes. This problem consists of proving that the parallel composition of an arbitrary number of processes running the same program (or a finite collection of programs) satisfies a temporal property. Our practical motivation is to build a general framework for the temporal verification of concurrent datatypes. In this paper we propose 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. Our method is based on a clear division between the following two dimensions of the problem: the interaction between executing threads—handled by novel parametrized invariance proof rules—, and the data being manipulated—handled by specialized decision procedures. Our proof rules discharge automatically a finite collection of verification conditions. The size of this collection depends only on the size of the program and the specification, but not on the number of processes in any given instance or on the kind of data manipulated. Moreover, all verification conditions are quantifier free, which eases the development of decision procedures for complex data-types on top of off-the-shelf SMT solvers. We prove soundness of our proof rules and illustrate their application in the formal verification of (1) two infinite-state mutual exclusion protocols; (2) shape and functional correctness properties of several concurrent data-types, including fine-grained and non-blocking concurrent lists and queues. We report empirical results using a prototype implementation of the proof rules and decision procedures.