From 2848951965ec258c225075f1ad00a3a7a337f0cc Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 10 Aug 2022 10:26:30 +0200
Subject: [PATCH] * doc/spot.bib: Add entries for last two tool papers.

---
 doc/spot.bib | 50 ++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 48 insertions(+), 2 deletions(-)

diff --git a/doc/spot.bib b/doc/spot.bib
index 2a58a3031..284bf226a 100644
--- a/doc/spot.bib
+++ b/doc/spot.bib
@@ -1,4 +1,3 @@
-
 @InProceedings{	  babiak.12.tacas,
   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
@@ -353,6 +352,41 @@
   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,
   author	= {Matthew B. Dwyer and George S. Avrunin and James C.
 		  Corbett},
@@ -1036,7 +1070,19 @@
   publisher	= {Elsevier},
   editor	= {Rance Cleaveland and Hubert Garavel},
   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},
   doi		= {10.1016/S1571-0661(04)80409-2}
 }