* doc/spot.bib: Add entries for last two tool papers.
This commit is contained in:
parent
a7e87a1fc7
commit
2848951965
1 changed files with 48 additions and 2 deletions
50
doc/spot.bib
50
doc/spot.bib
|
|
@ -1,4 +1,3 @@
|
||||||
|
|
||||||
@InProceedings{ babiak.12.tacas,
|
@InProceedings{ babiak.12.tacas,
|
||||||
author = {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r
|
author = {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r
|
||||||
K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k
|
K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k
|
||||||
|
|
@ -353,6 +352,41 @@
|
||||||
doi = {10.1504/IJCCBS.2014.059594}
|
doi = {10.1504/IJCCBS.2014.059594}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@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,
|
||||||
|
doi = {10.1007/978-3-319-46520-3_22}
|
||||||
|
}
|
||||||
|
|
||||||
|
@InProceedings{ duret.22.cav,
|
||||||
|
author = {Alexandre~Duret-Lutz and Etienne Renault and Maximilien
|
||||||
|
Colange and Florian Renkin and Alexandre Gbaguidi~Aisse and
|
||||||
|
Philipp Schlehuber-Caissier and Thomas Medioni and Antoine
|
||||||
|
Martin and J{\'e}r{\^o}me Dubois and Cl{\'e}ment Gillard
|
||||||
|
and Henrich Lauko},
|
||||||
|
title = {From {S}pot 2.0 to {S}pot 2.10: What's New?},
|
||||||
|
booktitle = {Proceedings of the 34th International Conference on
|
||||||
|
Computer Aided Verification (CAV'22)},
|
||||||
|
year = 2022,
|
||||||
|
volume = {13372},
|
||||||
|
series = {Lecture Notes in Computer Science},
|
||||||
|
pages = {174--187},
|
||||||
|
month = aug,
|
||||||
|
publisher = {Springer},
|
||||||
|
doi = {10.1007/978-3-031-13188-2_9}
|
||||||
|
}
|
||||||
|
|
||||||
@InProceedings{ dwyer.98.fmsp,
|
@InProceedings{ dwyer.98.fmsp,
|
||||||
author = {Matthew B. Dwyer and George S. Avrunin and James C.
|
author = {Matthew B. Dwyer and George S. Avrunin and James C.
|
||||||
Corbett},
|
Corbett},
|
||||||
|
|
@ -1036,7 +1070,19 @@
|
||||||
publisher = {Elsevier},
|
publisher = {Elsevier},
|
||||||
editor = {Rance Cleaveland and Hubert Garavel},
|
editor = {Rance Cleaveland and Hubert Garavel},
|
||||||
year = {2002},
|
year = {2002},
|
||||||
month = jul,
|
month = jul, pdf = {adl/duret.16.atva.pdf},
|
||||||
|
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.},
|
||||||
|
|
||||||
address = {M{\'a}laga, Spain},
|
address = {M{\'a}laga, Spain},
|
||||||
doi = {10.1016/S1571-0661(04)80409-2}
|
doi = {10.1016/S1571-0661(04)80409-2}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue