diff --git a/doc/org/satmin.org b/doc/org/satmin.org
index 4fc1244a8..f2f8c394c 100644
--- a/doc/org/satmin.org
+++ b/doc/org/satmin.org
@@ -31,8 +31,10 @@ Let us first state a few facts about this minimization procedure.
    automaton: when the number of clauses output by Spot (and to be fed
    to the SAT solver) exceeds $2^{31}$, or when the SAT-solver was
    killed by a signal.
+6) Details about the SAT encoding used in the two procedures can be
+   found in our [[http://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]].
 
-* How change the SAT solver used
+* How to change the SAT solver used
 
 The environment variable =SPOT_SATSOLVER= can be used to change the
 SAT solver used by Spot.  The default is "=glucose -verb=0 -model %I
diff --git a/doc/org/tools.org b/doc/org/tools.org
index 0d1cd597d..beccf501f 100644
--- a/doc/org/tools.org
+++ b/doc/org/tools.org
@@ -60,9 +60,9 @@ the following articles:
 
   This focuses on =ltlfilt=, =randltl=, and =ltlcross=.
 
-- *LTL translation improvements in Spot*, /Alexandre Duret-Lutz/.
-  In Proc. of VECoS'11.  Electronic Workshops in Computing. Tunis, Tunisia, Sep. 2011.
-  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.11.vecos][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.slides.pdf][slides]])
+- *LTL translation improvements in Spot 1.0*, /Alexandre Duret-Lutz/.
+  Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014.
+  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.14.ijccbs][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.14.ijccbs.draft.pdf][pdf]])
 
   This describes the translation from LTL to TGBA used by =ltl2tgba=
   and =ltl2tgta=.
diff --git a/src/bin/man/dstar2tgba.x b/src/bin/man/dstar2tgba.x
index ce7cec939..1198b6e94 100644
--- a/src/bin/man/dstar2tgba.x
+++ b/src/bin/man/dstar2tgba.x
@@ -2,7 +2,7 @@
 dstar2tgba \- convert Rabin or Streett automata into Büchi automata
 [BIBLIOGRAPHY]
 .TP
-1. 
+1.
 <http://www.ltl2dstar.de/docs/ltl2dstar.html>
 
 Documents the output format of ltl2dstar.
@@ -28,5 +28,15 @@ dstar2tgba implements this for the Rabin case only.  In other words,
 translating a deterministic Rabin automaton with dstar2tgba will
 produce a deterministic TGBA or BA if such a automaton exists.
 
+.TP
+4.
+Souheib Baarir and Alexandre Duret-Lutz: Mechanizing the minimization
+of deterministic generalized Büchi automata.  Proceedings of FORTE'14.
+LNCS 8461.
+
+Explains the SAT-based minimization techniques that can be used (on
+request only) by dstar2tgba to minimize deterministic Büchi automata.
+
+
 [SEE ALSO]
 .BR spot-x (7)
diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x
index 986e3a63d..3df465814 100644
--- a/src/bin/man/ltl2tgba.x
+++ b/src/bin/man/ltl2tgba.x
@@ -85,11 +85,22 @@ If you would like to give a reference to this tool in an article,
 we suggest you cite one of the following papers:
 .TP
 \(bu
-Alexandre Duret-Lutz: LTL translation improvements in Spot. Proceedings of VECoS'11.
+Alexandre Duret-Lutz: LTL translation improvements in Spot 1.0.
+Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014.
 .TP
 \(bu
 Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0.
 Proceedings of ATVA'13.  LNCS 8172.
+.TP
+\(bu
+Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský,
+and Jan Strejček: Compositional approach to suspension and other
+improvements to LTL translation.  Proceedings of SPIN'13.  LNCS 7976.
+.TP
+\(bu
+Souheib Baarir and Alexandre Duret-Lutz: Mechanizing the minimization
+of deterministic generalized Büchi automata.  Proceedings of FORTE'14.
+LNCS 8461.
 
 [SEE ALSO]
 .BR spot-x (7)