Difference between revisions of "Publications/fronc.13.atva"
From LRDE
| (9 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{Publication |
{{Publication |
||
| − | | |
+ | | published = true |
| + | | date = 2013-06-15 |
||
| authors = Łukasz Fronc, Alexandre Duret-Lutz |
| authors = Łukasz Fronc, Alexandre Duret-Lutz |
||
| title = LTL Model Checking with Neco |
| title = LTL Model Checking with Neco |
||
| Line 9: | Line 10: | ||
| address = Hanoi, Vietnam |
| address = Hanoi, Vietnam |
||
| publisher = Springer |
| publisher = Springer |
||
| − | | 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 |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/fronc.13.atva.pdf |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| + | | lrdenewsdate = 2013-06-15 |
||
| type = inproceedings |
| type = inproceedings |
||
| id = fronc.13.atva |
| id = fronc.13.atva |
||
| + | | identifier = doi:10.1007/978-3-319-02444-8_33 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> fronc.13.atva, |
@InProceedings<nowiki>{</nowiki> fronc.13.atva, |
||
| Line 24: | Line 26: | ||
year = 2013, |
year = 2013, |
||
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
||
| − | volume = |
+ | volume = 8172, |
pages = <nowiki>{</nowiki>451--454<nowiki>}</nowiki>, |
pages = <nowiki>{</nowiki>451--454<nowiki>}</nowiki>, |
||
address = <nowiki>{</nowiki>Hanoi, Vietnam<nowiki>}</nowiki>, |
address = <nowiki>{</nowiki>Hanoi, Vietnam<nowiki>}</nowiki>, |
||
| Line 36: | Line 38: | ||
architecture of Neco and explain how it was combined with |
architecture of Neco and explain how it was combined with |
||
Spot to build an LTL model checker.<nowiki>}</nowiki>, |
Spot to build an LTL model checker.<nowiki>}</nowiki>, |
||
| − | + | doi = <nowiki>{</nowiki>10.1007/978-3-319-02444-8_33<nowiki>}</nowiki> |
|
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 11:30, 1 April 2019
- 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.
Documents
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.},
doi = {10.1007/978-3-319-02444-8_33}
}