Difference between revisions of "Publications/fronc.13.atva"

From LRDE

 
Line 16: Line 16:
 
| 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 36: Line 37:
 
library of model-checking algorithms. We show the
 
library of model-checking algorithms. We show the
 
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 10:30, 1 April 2019

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}
}