Composition of accelerations to verify infinite heterogeneous systems

Abstract

Symbolic representations and acceleration algorithms are emerging methods to extend model-checking to infinite state space systems. However until now, there is no general theory of acceleration, and designing acceleration algorithms for new data types is a complex task. On the other hand, protocols rarely manipulate new data types, rather new combinations of well-studied data types. For this reason, in this paper we focus on the automatic construction of symbolic representations and acceleration algorithms from existing ones. © Springer-Verlag 2004.