Predicate Abstraction with Indexed Predicates

TL;DR

This paper introduces a predicate abstraction technique with indexed predicates for verifying infinite-state systems with first-order variables, including mutable functions and arrays, enabling the analysis of complex hardware and software models.

Contribution

It presents a novel form of predicate abstraction using universally quantified formulas to describe invariants in systems with first-order state variables, with formal soundness proof and practical verification applications.

Findings

Successfully verified hardware and software systems, including cache coherence protocols.

Formal proof of soundness for the proposed abstraction method.

Applicable to systems with arbitrarily large memories and arrays.

Abstract

Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model checking. We consider models containing first-order state variables, where the system state includes mutable functions and predicates. Such a model can describe systems containing arbitrarily large memories, buffers, and arrays of identical processes. We describe a form of predicate abstraction that constructs a formula over a set of universally quantified variables to describe invariant properties of the first-order state variables. We provide a formal justification of the soundness of our approach and describe how it has been used to verify several hardware and software designs, including a directory-based cache coherence protocol.