Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |

Download [help]

Download paper Adobe portable document format (pdf)

Copyright noticeThis 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.

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), Volume 3707 of LNCS},
   editor = {Springer, },
   Pages = {474--488},
   Address = {Taipei, Taiwan},
   Month = {October},
   Year = {2005}
}

EndNote Reference [help]

Get EndNote Reference (.ref)