loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
12th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS'04)
SPOT: An Extensible Model Checking Library Using Transition-Based Generalized B?chi Automata
Volendam, The Netherlands
October 04-October 08
ISBN: 0-7695-2251-3
ASCII Text
x 
 
Alexandre Duret-Lutz, Denis Poitrenaud, "SPOT: An Extensible Model Checking Library Using Transition-Based Generalized B?chi Automata," Modeling, Analysis, and Simulation of Computer Systems, International Symposium on, pp. 76-83, 12th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS'04), 2004.
 
 
BibTex
x
 
@article{ 10.1109/MASCOT.2004.1348184,
author = {Alexandre Duret-Lutz and Denis Poitrenaud},
title = {SPOT: An Extensible Model Checking Library Using Transition-Based Generalized B?chi Automata},
journal ={Modeling, Analysis, and Simulation of Computer Systems, International Symposium on},
volume = {0},
year = {2004},
issn = {1526-7539},
pages = {76-83},
doi = {http://doi.ieeecomputersociety.org/10.1109/MASCOT.2004.1348184},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Modeling, Analysis, and Simulation of Computer Systems, International Symposium on
TI - SPOT: An Extensible Model Checking Library Using Transition-Based Generalized B?chi Automata
SN - 1526-7539
SP76
EP83
A1 - Alexandre Duret-Lutz,
A1 - Denis Poitrenaud,
PY - 2004
KW - null
VL - 0
JA - Modeling, Analysis, and Simulation of Computer Systems, International Symposium on
ER -
 
Alexandre Duret-Lutz, Université P. & M. Curie
Denis Poitrenaud, Université P. & M. Curie
Spot is a C++ library offering model checking bricks that can be combined and interfaced with third party tools to build a model checker. It relies on Transition-based Generalized B?uchi Automata (TGBA) and does not need to degeneralize these automata to check their emptiness. We motivate the choice of TGBA by illustrating a very simple (yet efficient) translation of LTL into TGBA. We then show how it supports on-the-fly computations, and how it can be extended or integrated in other tools.
Citation:
Alexandre Duret-Lutz, Denis Poitrenaud, "SPOT: An Extensible Model Checking Library Using Transition-Based Generalized B?chi Automata," mascots, pp.76-83, 12th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.