Difference between revisions of "Publications/fronc.13.atva"
From LRDE
Line 12: | Line 12: | ||
| urllrde = 201310-ATVAb |
| urllrde = 201310-ATVAb |
||
| abstract = We introduce neco-spot, an LTL model checker for Petri net models. It builds upon Neco, a compiler turning Petri nets into native shared libraries that allows fast on-the-fly exploration of the state-space, and upon Spot, a C++ library of model-checking algorithms. We show the architecture of Neco and explain how it was combined with Spot to build an LTL model checker. |
| abstract = We introduce neco-spot, an LTL model checker for Petri net models. It builds upon Neco, a compiler turning Petri nets into native shared libraries that allows fast on-the-fly exploration of the state-space, and upon Spot, a C++ library of model-checking algorithms. We show the architecture of Neco and explain how it was combined with Spot to build an LTL model checker. |
||
− | | lrdepaper = http://www.lrde.epita.fr/dload/papers/fronc.13.atva.pdf |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2013-06-15 |
| lrdenewsdate = 2013-06-15 |
Revision as of 01:02, 10 March 2015
- Authors
- Łukasz Fronc, Alexandre Duret-Lutz
- Where
- Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13)
- Place
- Hanoi, Vietnam
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2013-06-15
Abstract
We introduce neco-spot, an LTL model checker for Petri net models. It builds upon Neco, a compiler turning Petri nets into native shared libraries that allows fast on-the-fly exploration of the state-space, and upon Spot, a C++ library of model-checking algorithms. We show the architecture of Neco and explain how it was combined with Spot to build an LTL model checker.
Bibtex (lrde.bib)
@InProceedings{ fronc.13.atva, author = {{\L}ukasz Fronc and Alexandre Duret-Lutz}, title = {{LTL} Model Checking with {N}eco}, booktitle = {Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13)}, year = 2013, series = {Lecture Notes in Computer Science}, volume = 8172, pages = {451--454}, address = {Hanoi, Vietnam}, month = oct, publisher = {Springer}, abstract = {We introduce neco-spot, an LTL model checker for Petri net models. It builds upon Neco, a compiler turning Petri nets into native shared libraries that allows fast on-the-fly exploration of the state-space, and upon Spot, a C++ library of model-checking algorithms. We show the architecture of Neco and explain how it was combined with Spot to build an LTL model checker.} }