\input zb-basic
\input zb-ioport
\iteman{io-port 05067791}
\itemau{Bardin, S\'ebastien; Finkel, Alain}
\itemti{Composition of accelerations to verify infinite heterogeneous systems.}
\itemso{Wang, Farn (ed.), Automated technology for verification and analysis. Second international conference, ATVA 2004, Taipei, Taiwan, ROC, October 31 -- November 3, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23610-4/pbk). Lecture Notes in Computer Science 3299, 248-262 (2004).}
\itemab
Summary: 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.
\itemrv{~}
\itemcc{}
\itemut{reachability set; unbounded heterogeneous data; composition of symbolic representations and acceleration methods}
\itemli{doi:10.1007/b102065}
\end