The Spotlight Principle

Abstract

Formal verification of safety and liveness properties of systems with a dynamically changing, unbounded number of interlinked processes and infinite-domain local data is challenging due to the two sources of infiniteness. The existing state abstraction-based approaches Data Type Reduction and Environment Abstraction each address one aspect, but the former doesn’t support infinite-domain local data and the latter doesn’t support links and is restricted to particular properties. The contribution of this paper is a combination of both which is obtained by first stating them in the framework of Canonical Abstraction. This new use of Canonical Abstraction, originally designed and used for the analysis of programs with heap-allocated data structures, furthermore unveils a formal connection between the two rather ad-hoc techniques.