×

zbMATH — the first resource for mathematics

Flat acceleration in symbolic model checking. (English) Zbl 1170.68507
Peled, Doron A. (ed.) et al., Automated technology for verification and analysis. Third international symposium, ATVA 2005, Taipei, Taiwan, October 4–7, 2005. Proceedings. Berlin: Springer (ISBN 3-540-29209-8/pbk). Lecture Notes in Computer Science 3707, 474-488 (2005).
Summary: Symbolic model checking provides partially effective verification procedures that can handle systems with an infinite state space. So-called “acceleration techniques” enhance the convergence of fixpoint computations by computing the transitive closure of some transitions. In this paper we develop a new framework for symbolic model checking with accelerations. We also propose and analyze new symbolic algorithms using accelerations to compute reachability sets.
For the entire collection see [Zbl 1089.68013].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
TREX
PDF BibTeX XML Cite
Full Text: DOI