Difference between revisions of "Publications/fronc.13.atva"
From LRDE
(Created page with "{{Publication | date = 2013-10-01 | authors = Łukasz Fronc, Alexandre Duret-Lutz | title = LTL Model Checking with Neco | booktitle = Proceedings of the 11th International Sy...") |
|||
| Line 5: | Line 5: | ||
| booktitle = Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13) |
| booktitle = Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13) |
||
| series = Lecture Notes in Computer Science |
| series = Lecture Notes in Computer Science |
||
| − | | volume = |
+ | | volume = 8172 |
| − | | pages = |
+ | | pages = 451 to 454 |
| − | | notes = To appear |
||
| address = Hanoi, Vietnam |
| address = Hanoi, Vietnam |
||
| publisher = Springer |
| publisher = Springer |
||
| 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 Spota 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 Spota 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 |
||
| type = inproceedings |
| type = inproceedings |
||
| id = fronc.13.atva |
| id = fronc.13.atva |
||
| Line 17: | Line 17: | ||
@InProceedings<nowiki>{</nowiki> fronc.13.atva, |
@InProceedings<nowiki>{</nowiki> fronc.13.atva, |
||
author = <nowiki>{</nowiki><nowiki>{</nowiki>\L<nowiki>}</nowiki>ukasz Fronc and Alexandre Duret-Lutz<nowiki>}</nowiki>, |
author = <nowiki>{</nowiki><nowiki>{</nowiki>\L<nowiki>}</nowiki>ukasz Fronc and Alexandre Duret-Lutz<nowiki>}</nowiki>, |
||
| − | title = <nowiki>{</nowiki>LTL Model Checking with |
+ | title = <nowiki>{</nowiki><nowiki>{</nowiki>LTL<nowiki>}</nowiki> Model Checking with <nowiki>{</nowiki>N<nowiki>}</nowiki>eco<nowiki>}</nowiki>, |
booktitle = <nowiki>{</nowiki>Proceedings of the 11th International Symposium on |
booktitle = <nowiki>{</nowiki>Proceedings of the 11th International Symposium on |
||
Automated Technology for Verification and Analysis |
Automated Technology for Verification and Analysis |
||
| Line 23: | Line 23: | ||
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 = <nowiki>{</nowiki> |
+ | volume = <nowiki>{</nowiki>8172<nowiki>}</nowiki>, |
| − | pages = <nowiki>{</nowiki> |
+ | pages = <nowiki>{</nowiki>451--454<nowiki>}</nowiki>, |
| − | notes = <nowiki>{</nowiki>To appear<nowiki>}</nowiki>, |
||
address = <nowiki>{</nowiki>Hanoi, Vietnam<nowiki>}</nowiki>, |
address = <nowiki>{</nowiki>Hanoi, Vietnam<nowiki>}</nowiki>, |
||
month = oct, |
month = oct, |
||
Revision as of 15:30, 25 October 2013
- 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
- Date
- 2013-10-01
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 Spota 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.}
}