一句话：提出索引谓词抽象，将数组系统过近似为字符串重写系统，从而自动验证安全性与活性。
本文关注数组系统的安全性与活性验证。数组系统可自然刻画进程数无界的参数化分布式协议，且进程常使用无界域上的进程 ID，使验证极具挑战。作者提出一种基于索引谓词的新型谓词抽象，将数组系统过近似为有限字母表上的字符串重写系统；由此可复用过去二十年发展的字符串重写系统验证技术，特别是正则模型检测。该方法能为 Dijkstra 自稳定协议和 Chang-Roberts 领导者选举协议等难题给出简单且可自动检查的安全性/活性证明。
Verifying safety and liveness over array systems is a highly challenging problem. Array systems naturally capture parameterized systems such as distributed protocols with an unbounded number of processes. Such distributed protocols often exploit process IDs during their computation, resulting in array systems whose element values range over an infinite domain. In this paper, we develop a novel framework for proving safety and liveness over array systems. The crux of the framework is to overapproximate an array system as a string rewriting system (i.e. over a finite alphabet) by means of a new predicate abstraction that exploits the so-called indexed predicates. This allows us to tap into powerful verification methods for string rewriting systems that have been heavily developed in the last two decades or so (e.g. regular model checking). We demonstrate how our method yields simple, automatically verifiable proofs of safety and liveness properties for challenging examples, including Dijkstra’s self-stabilizing protocol and the Chang-Roberts leader election protocol.