diff --git a/ChangeLog b/ChangeLog
index a578b3826..c254b4f15 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,8 @@
+2010-01-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	* README: Add descriptions for subdirectories of bench/, src/sanity,
+	and src/kripke.
+
 2010-01-24  Guillaume Sadegh  <sadegh@lrde.epita.fr>
 
 	* src/sanity/readme.test: A script to check whether all the
diff --git a/README b/README
index af86c69ec..d9ce9e799 100644
--- a/README
+++ b/README
@@ -92,46 +92,52 @@ Layout of the source tree
 Core directories
 ----------------
 
-src/            Sources for libspot.
-   ltlast/      LTL abstract syntax tree (including nodes for ELTL).
-   ltlenv/      LTL environments.
-   ltlparse/    Parser for LTL formulae.
-   ltlvisit/    Visitors of LTL formulae.
-   ltltest/     Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/.
-   misc/        Miscellaneous support files.
-   tgba/        TGBA objects and cousins.
-   tgbaalgos/   Algorithms on TGBA.
-      gtec/     Couvreur's Emptiness-Check.
-   tgbaparse/   Parser for explicit TGBA.
-   tgbatest/    Tests for tgba/, tgbaalgos/, and tgbaparse/.
-   evtgba*/     Ignore these for now.
-   eltlparse/	Parser for ELTL formulae.
-   eltltest/    Tests for ELTL nodes in ltlast/ and eltlparse/.
-   saba/        SABA (State-labeled Alternating Büchi Automata) objects.
-   sabaalgos/   Algorithms on SABA.
-   sabatest/    Tests for saba/, sabaalgos/.
-doc/	        Documentation for libspot.
-   spot.html/   HTML reference manual.
-   spot.latex/  Sources for the PDF manual.  (Not distributed, can be rebuilt.)
-   spotref.pdf  PDF reference manual.
-bench/          Benchmarks...
-   emptchk/     ... for emptiness-check algorithms,
-   ltl2tgba/    ... for LTL-to-Büchi translation algorithms.
-wrap/	        Wrappers for other languages.
-   python/      Python bindings for Spot and BuDDy
-      tests/    Tests for these bindings
-      cgi/      Python-based CGI script (ltl-to-tgba translator)
-iface/	        Interfaces to other libraries.
-   gspn/        GreatSPN interface.
-      examples/ Supporting models used by the test cases.
-   nips/        NIPS interface (to use Promela models).
-      nipstest/ Tests for NIPS.
+src/              Sources for libspot.
+   kripke/	  Kripke Structure interface.
+   ltlast/        LTL abstract syntax tree (including nodes for ELTL).
+   ltlenv/        LTL environments.
+   ltlparse/      Parser for LTL formulae.
+   ltlvisit/      Visitors of LTL formulae.
+   ltltest/       Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/.
+   misc/          Miscellaneous support files.
+   tgba/          TGBA objects and cousins.
+   tgbaalgos/     Algorithms on TGBA.
+      gtec/       Couvreur's Emptiness-Check.
+   tgbaparse/     Parser for explicit TGBA.
+   tgbatest/      Tests for tgba/, tgbaalgos/, and tgbaparse/.
+   evtgba*/       Ignore these for now.
+   eltlparse/	  Parser for ELTL formulae.
+   eltltest/      Tests for ELTL nodes in ltlast/ and eltlparse/.
+   saba/          SABA (State-labeled Alternating Büchi Automata) objects.
+   sabaalgos/     Algorithms on SABA.
+   sabatest/      Tests for saba/, sabaalgos/.
+   sanity/        Sanity tests for the whole project.
+doc/	          Documentation for libspot.
+   spot.html/     HTML reference manual.
+   spot.latex/    Sources for the PDF manual.  (Not distributed, can be rebuilt.)
+   spotref.pdf    PDF reference manual.
+bench/            Benchmarks for ...
+   emptchk/       ... emptiness-check algorithms,
+   gspn-ssp/      ... various symmetry-based methods with GreatSPN,
+   ltl2tgba/      ... LTL-to-Büchi translation algorithms,
+   ltlcouter/     ... translation of a class of LTL formulae,
+   scc-stats/     ... SCC statistics after translation of LTL formulae,
+   split-product/ ... parallelizing gain after splitting LTL automata.
+wrap/	          Wrappers for other languages.
+   python/        Python bindings for Spot and BuDDy
+      tests/      Tests for these bindings
+      cgi/        Python-based CGI script (ltl-to-tgba translator)
+iface/	          Interfaces to other libraries.
+   gspn/          GreatSPN interface.
+      examples/   Supporting models used by the test cases.
+   nips/          NIPS interface (to use Promela models).
+      nipstest/   Tests for NIPS.
 
 Third party software
 --------------------
 
 buddy/            A patched version of BuDDy 2.3 (a BDD library).
-lbtt/             lbtt 1.2.0 (an LTL to Büchi automata test bench).
+lbtt/             lbtt 1.2.1 (an LTL to Büchi automata test bench).
 iface/            Interfaces to other libraries.
    nips/          NIPS interface (to use Promela models).
       nips_vm/    NIPS VM 1.2.7 (New Implementation of Promela Semantics
@@ -151,5 +157,7 @@ End:
  LocalWords:  Python's BuDDy LBTT LTL Büchi lbtt gspn DIR GreatSPN Soheib Yann
  LocalWords:  Baarir Thierry Mieg CVS Università di Torino devel src libspot ac
  LocalWords:  ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos
- LocalWords:  gtec Tarjan tgbaparse tgbatest doc html PDF spotref pdf cgi
- LocalWords:  CGI ltl iface BDD Couvreur's evtgba emptchk
+ LocalWords:  gtec Tarjan tgbaparse tgbatest doc html PDF spotref pdf cgi ELTL
+ LocalWords:  CGI ltl iface BDD Couvreur's evtgba emptchk kripke Kripke saba vm
+ LocalWords:  eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC
+ LocalWords:  Promela nipstest VM