leroux05b

S. Bardin, A. Finkel, J. Leroux, P. Schnoebelen. Flat acceleration in symbolic model checking. In 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05), Springer (ed.), LNCS, Volume 3707, Pages 474-488, Taipei, Taiwan, October 2005.

Download [help]

Download paper: Doi page

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

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. Keywords: verification of infinite-state systems, symbolic model checking, acceleration

BibTex Reference

@InProceedings{leroux05b,
   Author = {Bardin, S. and Finkel, A. and Leroux, J. and Schnoebelen, P.},
   Title = {Flat acceleration in symbolic model checking},
   BookTitle = {3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05)},
   editor = {Springer, },
   Volume = {    3707},
   Pages = {474--488},
   Series = {LNCS},
   Address = {Taipei, Taiwan},
   Month = {October},
   Year = {2005}
}

EndNote Reference [help]

Get EndNote Reference (.ref)