Difference between revisions of "Publications/duret.16.atva"

From LRDE

(Created page with "{{Publication | published = true | date = 2016-10-01 | authors = Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Etienne Renault | title = Heuristics for Checking Live...")
 
 
(7 intermediate revisions by the same user not shown)
Line 1: Line 1:
 
{{Publication
  
{{Publication
 
| published = true
  
| published = true
−
| date = 2016-10-01
 +
| date = 2016-06-17
 
| authors = Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Etienne Renault
  
| authors = Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Etienne Renault
 
| title = Heuristics for Checking Liveness Properties with Partial Order Reductions
  
| title = Heuristics for Checking Liveness Properties with Partial Order Reductions
Line 7: Line 7:
 
| series = Lecture Notes in Computer Science
  
| series = Lecture Notes in Computer Science
 
| publisher = Springer
  
| publisher = Springer
−
| volume = ????
 +
| volume = 9938
−
| pages = ?? to ??
 +
| pages = 340 to 356
−
| abstract = Checking liveness properties with partial-order reductions requires a cycle proviso to ensure that an action cannot be postponed forever. The proviso forces each cycle to contain at least one fully expanded state. We present new heuristics to select which state to expand, hoping to reduce the size of the resulting graph. The choice of the state to expand is done when encountering a dangerous edge. Almost all existing provisos expand the source of this edge, while this paper also explores the expansion of the destination and the use of SCC-based information.
 +
| abstract = Checking liveness properties with partial-order reductions requires a cycle proviso to ensure that an action cannot be postponed forever. The proviso forces each cycle to contain at least one fully expanded state. We present new heuristics to select which state to expand, hoping to reduce the size of the resulting graph. The choice of the state to expand is done when encountering a dangerous edge. Almost all existing provisos expand the source of this edge, while this paper also explores the expansion of the destination and the use of SCC-based information.
 
| lrdeprojects = Spot
  
| lrdeprojects = Spot
  +
| lrdepaper = http://www.lrde.epita.fr/dload/papers/duret.16.atva.pdf
−
| lrdenewsdate = 2016-06-17 note = To appear.
 +
| lrdenewsdate = 2016-06-17
 
| type = inproceedings
  
| type = inproceedings
 
| id = duret.16.atva
  
| id = duret.16.atva
  +
| identifier = doi:10.1007/978-3-319-46520-3_22
 
| bibtex =
 
| bibtex =
 
@InProceedings<nowiki>{</nowiki> duret.16.atva,
  
@InProceedings<nowiki>{</nowiki> duret.16.atva,
Line 25: Line 27:
 
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
  
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
 
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
  
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
−
volume = <nowiki>{</nowiki>????<nowiki>}</nowiki>,
 +
volume = <nowiki>{</nowiki>9938<nowiki>}</nowiki>,
−
pages = <nowiki>{</nowiki>??--??<nowiki>}</nowiki>,
 +
pages = <nowiki>{</nowiki>340--356<nowiki>}</nowiki>,
 
year = <nowiki>{</nowiki>2016<nowiki>}</nowiki>,
  
year = <nowiki>{</nowiki>2016<nowiki>}</nowiki>,
 
month = oct,
  
month = oct,
Line 40: Line 42:
 
expansion of the destination and the use of SCC-based
  
expansion of the destination and the use of SCC-based
 
information.<nowiki>}</nowiki>,
  
information.<nowiki>}</nowiki>,
−
note = <nowiki>{</nowiki>To appear.<nowiki>}</nowiki>
 +
doi = <nowiki>{</nowiki>10.1007/978-3-319-46520-3_22<nowiki>}</nowiki>
−
<nowiki>}</nowiki>
  
−  
−
@InProceedings<nowiki>{</nowiki> duret.16.atva2,
  
−
author = <nowiki>{</nowiki>Alexandre Duret-Lutz and Alexandre Lewkowicz and Amaury
  
−
Fauchille and Thibaud Michaud and Etienne Renault and
  
−
Laurent Xu<nowiki>}</nowiki>,
  
−
title = <nowiki>{</nowiki>Spot 2.0 --- a framework for <nowiki>{</nowiki>LTL<nowiki>}</nowiki> and $\omega$-automata
  
−
manipulation<nowiki>}</nowiki>,
  
−
booktitle = <nowiki>{</nowiki>Proceedings of the 14th International Symposium on
  
−
Automated Technology for Verification and Analysis
  
−
(ATVA'16)<nowiki>}</nowiki>,
  
−
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
  
−
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
  
−
volume = <nowiki>{</nowiki>????<nowiki>}</nowiki>,
  
−
pages = <nowiki>{</nowiki>??--??<nowiki>}</nowiki>,
  
−
year = <nowiki>{</nowiki>2016<nowiki>}</nowiki>,
  
−
month = oct,
  
−
pdf = <nowiki>{</nowiki>adl/duret.16.atva2.pdf<nowiki>}</nowiki>,
  
−
abstract = <nowiki>{</nowiki>We present Spot 2.0, a C++ library with Python bindings
  
−
and an assortment of command-line tools designed to
  
−
manipulate LTL and $\omega$-automata in batch. New
  
−
automata-manipulation tools were introduced in Spot 2.0;
  
−
they support arbitrary acceptance conditions, as
  
−
expressible in the Hanoi Omega Automaton format. Besides
  
−
being useful to researchers who have automata to process,
  
−
its Python bindings can also be used in interactive
  
−
environments to teach $\omega$-automata and model checking.<nowiki>}</nowiki>,
  
−
note = <nowiki>{</nowiki>To appear.<nowiki>}</nowiki>
  
 
<nowiki>}</nowiki>
  
<nowiki>}</nowiki>
   

Latest revision as of 11:30, 1 April 2019

Authors
Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Etienne Renault
Where
Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16)
Type
inproceedings
Publisher
Springer
Projects
Spot
Date
2016-06-17

Abstract

Checking liveness properties with partial-order reductions requires a cycle proviso to ensure that an action cannot be postponed forever. The proviso forces each cycle to contain at least one fully expanded state. We present new heuristics to select which state to expand, hoping to reduce the size of the resulting graph. The choice of the state to expand is done when encountering a dangerous edge. Almost all existing provisos expand the source of this edge, while this paper also explores the expansion of the destination and the use of SCC-based information.

Documents

Bibtex (lrde.bib)

@InProceedings{	  duret.16.atva,
  author	= {Alexandre Duret-Lutz and Fabrice Kordon and Denis
		  Poitrenaud and Etienne Renault},
  title		= {Heuristics for Checking Liveness Properties with Partial
		  Order Reductions},
  booktitle	= {Proceedings of the 14th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'16)},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer},
  volume	= {9938},
  pages		= {340--356},
  year		= {2016},
  month		= oct,
  abstract	= {Checking liveness properties with partial-order reductions
		  requires a cycle proviso to ensure that an action cannot be
		  postponed forever. The proviso forces each cycle to contain
		  at least one fully expanded state. We present new
		  heuristics to select which state to expand, hoping to
		  reduce the size of the resulting graph. The choice of the
		  state to expand is done when encountering a
		  \emph{dangerous} edge. Almost all existing provisos expand
		  the source of this edge, while this paper also explores the
		  expansion of the destination and the use of SCC-based
		  information.},
  doi		= {10.1007/978-3-319-46520-3_22}
}





Retrieved from "https://www.lrde.epita.fr/index.php?title=Publications/duret.16.atva&oldid=123237"