• français
    • English
  • English 
    • français
    • English
  • Login
JavaScript is disabled for your browser. Some features of this site may not work without it.
BIRD Home

Browse

This CollectionBy Issue DateAuthorsTitlesSubjectsJournals BIRDResearch centres & CollectionsBy Issue DateAuthorsTitlesSubjectsJournals

My Account

Login

Statistics

View Usage Statistics

Design and Evaluation of a Symbolic and Abstraction-Based Model Checker

Thumbnail
Date
2004
Collection title
Lecture Notes in Computer Science
Collection Id
3299
Dewey
Informatique générale
Sujet
OBDD; Model Checking; Abstraction
DOI
http://dx.doi.org/10.1007/978-3-540-30476-0_19
Conference name
2nd International Symposium on Automated Technology for Verification and Analysis, ATVA 2004
Conference date
10-2004
Conference city
Taipei
Conference country
Taïwan
Book title
Automated Technology for Verification and Analysis Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31 - November 3, 2004. Proceedings
Author
Wang, Farn
Publisher
Springer
Publisher city
Berlin
Year
2004
Pages number
506
ISBN
978-3-540-23610-8
Book URL
http://dx.doi.org/10.1007/b102065
URI
https://basepub.dauphine.fr/handle/123456789/5207
Collections
  • LAMSADE : Publications
Metadata
Show full item record
Author
Haddad, Serge
Ilié, Jean-Michel
Klai, Kais
Type
Communication / Conférence
Item number of pages
196-210
Abstract (EN)
Symbolic model-checking usually includes two steps: the building of a compact representation of a state graph and the evaluation of the properties of the system upon this data structure. In case of properties expressed with a linear time logic, it appears that the second step is often more time consuming than the first one. In this work, we present a mixed solution which builds an observation graph represented in a non symbolic way but where the nodes are essentially symbolic set of states. Due to the small number of events to be observed in a typical formula, this graph has a very moderate size and thus the complexity time of verification is neglectible w.r.t. the time to build the observation graph. Thus we propose different symbolic implementations for the construction of the nodes of this graph. The evaluations we have done on standard examples show that our method outperforms the pure symbolic methods which makes it attractive.

  • Accueil Bibliothèque
  • Site de l'Université Paris-Dauphine
  • Contact
SCD Paris Dauphine - Place du Maréchal de Lattre de Tassigny 75775 Paris Cedex 16

 Content on this site is licensed under a Creative Commons 2.0 France (CC BY-NC-ND 2.0) license.