diff --git a/ChangeLog b/ChangeLog
index 2ccd78d8a..2d3e2b4b3 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,16 @@
 2003-12-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/ltltest/defs.in (run): New function, run valgrind.
+	* src/ltltest/equals.test, src/ltltest/lunabbrev.test,
+	src/ltltest/nenoform.test, src/ltltest/parse.test,
+	src/ltltest/parseerr.test, src/ltltest/tostring.test,
+	src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test: Use run().
+	* Makefile.am (EXTRA_DIST): Don't list the m4/*.m4 files,
+	Automake 1.8 find them automatically.
+	* configure.ac: Require Automake 1.8, in gnits mode, and check
+	for valgrind.
+	* THANKS: New empty file.
+
 	* doc/Doxyfile.in: Upgrade to Doxygen 1.3.5.  Build
 	documentation for iface/.
 	* dox/mainpage.dox: Fix reference to ltl_to_tgba.
diff --git a/HACKING b/HACKING
index 87c5078c9..202fd119d 100644
--- a/HACKING
+++ b/HACKING
@@ -10,11 +10,11 @@ Here are the tools you need to bootstrap the CVS tree, or more
 generally if you plan to regenerate some of the generated files.
 
   GNU Autoconf 2.57
-  GNU Automake 1.7.8
+  GNU Automake 1.8
   GNU Flex (the version probably doesn't matter much, we used 2.5.4)
   The CVS version of GNU Bison (called 1.875b at the time of writing)
   SWIG 1.3.19
-  Doxygen 1.3.4
+  Doxygen 1.3.5
 
 Bootstrap the CVS tree by running
 
diff --git a/Makefile.am b/Makefile.am
index c0d18321b..6505df1a4 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -29,14 +29,4 @@ endif WITH_INCLUDED_LBTT
 SUBDIRS = $(MAYBE_BUDDY) $(MAYBE_LBTT) doc src wrap iface
 
 ACLOCAL_AMFLAGS = -I m4
-EXTRA_DIST = \
-  m4/buddy.m4 \
-  m4/debug.m4 \
-  m4/devel.m4 \
-  m4/gccoptim.m4 \
-  m4/gccwarn.m4 \
-  m4/gspnlib.m4 \
-  m4/lbtt.m4 \
-  m4/ndebug.m4 \
-  m4/pypath.m4 \
-  HACKING
+EXTRA_DIST = HACKING
diff --git a/THANKS b/THANKS
new file mode 100644
index 000000000..e69de29bb
diff --git a/configure.ac b/configure.ac
index 748170dda..66b004ffe 100644
--- a/configure.ac
+++ b/configure.ac
@@ -22,7 +22,7 @@
 AC_PREREQ([2.57])
 AC_INIT([spot], [0.0m])
 AC_CONFIG_AUX_DIR([tools])
-AM_INIT_AUTOMAKE([nostdinc check-news 1.7.3])
+AM_INIT_AUTOMAKE([gnits nostdinc 1.8])
 
 adl_ENABLE_DEVEL
 adl_CHECK_PYTHON
@@ -46,6 +46,7 @@ ad_GCC_OPTIM
 adl_NDEBUG
 
 AC_CHECK_PROG([DOT], [dot], [dot])
+AC_CHECK_PROG([VALGRIND], [valgrind], [valgrind])
 
 AC_CONFIG_FILES([
   Makefile
diff --git a/src/ltltest/defs.in b/src/ltltest/defs.in
index ed33a95cd..d31c9ea95 100644
--- a/src/ltltest/defs.in
+++ b/src/ltltest/defs.in
@@ -46,6 +46,26 @@ test -z "$VERBOSE" && exec >/dev/null 2>&1
 echo "== Running test $0"
 
 DOT='@DOT@'
+VALGRIND='@VALGRIND@'
+
+run()
+{
+  expected_exitcode=$1
+  shift
+  exitcode=0
+  if test -n "$VALGRIND"; then
+    exec 6>valgrind.err
+    # No --leak-check=yes for now, as it causes parserr.test to fail.
+    GLIBCPP_FORCE_NEW=1 \
+    $VALGRIND --logfile-fd=6 -q "$@" || exitcode=$?
+    cat valgrind.err 1>&2
+    test -z "`sed 1q valgrind.err`" || exit 50
+    rm -f valgrind.err
+  else
+    "$@" || exitcode $?
+  fi
+  test $exitcode = $expected_exitcode || exit 1
+}
 
 # Turn on shell traces when VERBOSE=x.
 if test "x$VERBOSE" = xx; then
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index 431b1ce29..ceb700e34 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -25,42 +25,33 @@
 
 . ./defs || exit 1
 
-check()
-{
-  ./equals "$2" "$3"
-  test $? != $1 && exit 1;
-}
-
 # A few things which are equal
-check 0 'a' 'a'
-check 0 '1' '1'
-check 0 '0' '0'
-check 0 'a => b' 'a => b'
-check 0 'G a ' ' G a'
-check 0 'a U b' 'a U b'
-check 0 'a & b' 'a & b'
-check 0 'a & b' 'b & a'
-check 0 'a & b & c' 'c & a && b'
-check 0 'a & b & c' 'b & c & a'
-check 0 'a && b & a' 'b & a & b'
-check 0 'a & b' 'b & a & b'
-check 0 'a & b' 'b & a & a'
-check 0 'a & b & (c |(f U g)|| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
-check 0 'a & a' 'a'
+run 0 ./equals 'a' 'a'
+run 0 ./equals '1' '1'
+run 0 ./equals '0' '0'
+run 0 ./equals 'a => b' 'a => b'
+run 0 ./equals 'G a ' ' G a'
+run 0 ./equals 'a U b' 'a U b'
+run 0 ./equals 'a & b' 'a & b'
+run 0 ./equals 'a & b' 'b & a'
+run 0 ./equals 'a & b & c' 'c & a && b'
+run 0 ./equals 'a & b & c' 'b & c & a'
+run 0 ./equals 'a && b & a' 'b & a & b'
+run 0 ./equals 'a & b' 'b & a & b'
+run 0 ./equals 'a & b' 'b & a & a'
+run 0 ./equals 'a & b & (c |(f U g)|| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
+run 0 ./equals 'a & a' 'a'
 
 # other formulae which are not
-check 1 'a' 'b'
-check 1 '1' '0'
-check 1 'a => b' 'b => a'
-check 1 'a => b' 'a <=> b'
-check 1 'a => b' 'a U b'
-check 1 'a R b' 'a U b'
-check 1 'a & b & c' 'c & a'
-check 1 'b & c' 'c & a & b'
-check 1 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(g U g)| e | c) & b'
+run 1 ./equals 'a' 'b'
+run 1 ./equals '1' '0'
+run 1 ./equals 'a => b' 'b => a'
+run 1 ./equals 'a => b' 'a <=> b'
+run 1 ./equals 'a => b' 'a U b'
+run 1 ./equals 'a R b' 'a U b'
+run 1 ./equals 'a & b & c' 'c & a'
+run 1 ./equals 'b & c' 'c & a & b'
+run 1 ./equals 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(g U g)| e | c) & b'
 
 # Precedence
-check 0 'a & b ^ c | d' 'd | c ^ b & a'
-
-# Success.
-:
+run 0 ./equals 'a & b ^ c | d' 'd | c ^ b & a'
diff --git a/src/ltltest/lunabbrev.test b/src/ltltest/lunabbrev.test
index 7fe9b8606..e22a4e8c1 100755
--- a/src/ltltest/lunabbrev.test
+++ b/src/ltltest/lunabbrev.test
@@ -28,22 +28,22 @@
 set -e
 
 # A few things that do not change
-./lunabbrev 'a' 'a'
-./lunabbrev '1' '1'
-./lunabbrev '0' '0'
-./lunabbrev 'G a ' ' G a'
-./lunabbrev 'a U b' 'a U b'
-./lunabbrev 'a & b' 'a & b'
-./lunabbrev 'a & b' 'b & a'
-./lunabbrev 'a & b & c' 'c & a & b'
-./lunabbrev 'a & b & c' 'b & c & a'
-./lunabbrev 'a & b & a' 'b & a & b'
-./lunabbrev 'a & b' 'b & a & b'
-./lunabbrev 'a & b' 'b & a & a'
-./lunabbrev 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
+run 0 ./lunabbrev 'a' 'a'
+run 0 ./lunabbrev '1' '1'
+run 0 ./lunabbrev '0' '0'
+run 0 ./lunabbrev 'G a ' ' G a'
+run 0 ./lunabbrev 'a U b' 'a U b'
+run 0 ./lunabbrev 'a & b' 'a & b'
+run 0 ./lunabbrev 'a & b' 'b & a'
+run 0 ./lunabbrev 'a & b & c' 'c & a & b'
+run 0 ./lunabbrev 'a & b & c' 'b & c & a'
+run 0 ./lunabbrev 'a & b & a' 'b & a & b'
+run 0 ./lunabbrev 'a & b' 'b & a & b'
+run 0 ./lunabbrev 'a & b' 'b & a & a'
+run 0 ./lunabbrev 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
 # other formulae that do change
-./lunabbrev 'a ^ b' '(a & !b) | (!a & b)'
-./lunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
-./lunabbrev 'GF a => F G(b)' '!GFa | F Gb'
-./lunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
-./lunabbrev '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
+run 0 ./lunabbrev 'a ^ b' '(a & !b) | (!a & b)'
+run 0 ./lunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
+run 0 ./lunabbrev 'GF a => F G(b)' '!GFa | F Gb'
+run 0 ./lunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
+run 0 ./lunabbrev '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
diff --git a/src/ltltest/nenoform.test b/src/ltltest/nenoform.test
index a9edadfb8..ee105adb7 100755
--- a/src/ltltest/nenoform.test
+++ b/src/ltltest/nenoform.test
@@ -28,37 +28,37 @@
 set -e
 
 # A few things that do not change
-./nenoform 'a' 'a'
-./nenoform '1' '1'
-./nenoform '0' '0'
-./nenoform '!a' '!a'
-./nenoform 'a U b' 'a U b'
-./nenoform 'a & b' 'a & b'
-./nenoform 'a & b' 'b & a'
-./nenoform 'a & !b & c' 'c & a & !b'
-./nenoform 'a & b & c' 'b & c & a'
-./nenoform 'Xa & b & Xa' 'b & Xa & b'
-./nenoform 'a & b' 'b & a & b'
-./nenoform 'a & !b' '!b & a & a'
-./nenoform 'a & b & (Xc |(f U !g)| e)' 'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
-./nenoform 'GFa => FGb' 'GFa => FGb'
+run 0 ./nenoform 'a' 'a'
+run 0 ./nenoform '1' '1'
+run 0 ./nenoform '0' '0'
+run 0 ./nenoform '!a' '!a'
+run 0 ./nenoform 'a U b' 'a U b'
+run 0 ./nenoform 'a & b' 'a & b'
+run 0 ./nenoform 'a & b' 'b & a'
+run 0 ./nenoform 'a & !b & c' 'c & a & !b'
+run 0 ./nenoform 'a & b & c' 'b & c & a'
+run 0 ./nenoform 'Xa & b & Xa' 'b & Xa & b'
+run 0 ./nenoform 'a & b' 'b & a & b'
+run 0 ./nenoform 'a & !b' '!b & a & a'
+run 0 ./nenoform 'a & b & (Xc |(f U !g)| e)' 'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
+run 0 ./nenoform 'GFa => FGb' 'GFa => FGb'
 
 # Basic rewritings
-./nenoform '!!a' 'a'
-./nenoform '!!!!!a' '!a'
-./nenoform '!Xa' 'X!a'
-./nenoform '!Fa' 'G!a'
-./nenoform '!Ga' 'F!a'
-./nenoform '!(a ^ b)' 'a <=> b'
-./nenoform '!(a <=> b)' '(((a) ^ (b)))'
-./nenoform '!(a => b)' 'a&!b'
-./nenoform '!(!a => !b)' '!a&b'
-./nenoform '!(a U b)' '!a R !b'
-./nenoform '!(a R b)' '!a U !b'
-./nenoform '!(!a R !b)' 'a U b'
-./nenoform '!(a & b & c & d & b)' '!a | !b | !c | !d'
-./nenoform '!(a | b | c | d)' '!a & !b & !c & !d'
+run 0 ./nenoform '!!a' 'a'
+run 0 ./nenoform '!!!!!a' '!a'
+run 0 ./nenoform '!Xa' 'X!a'
+run 0 ./nenoform '!Fa' 'G!a'
+run 0 ./nenoform '!Ga' 'F!a'
+run 0 ./nenoform '!(a ^ b)' 'a <=> b'
+run 0 ./nenoform '!(a <=> b)' '(((a) ^ (b)))'
+run 0 ./nenoform '!(a => b)' 'a&!b'
+run 0 ./nenoform '!(!a => !b)' '!a&b'
+run 0 ./nenoform '!(a U b)' '!a R !b'
+run 0 ./nenoform '!(a R b)' '!a U !b'
+run 0 ./nenoform '!(!a R !b)' 'a U b'
+run 0 ./nenoform '!(a & b & c & d & b)' '!a | !b | !c | !d'
+run 0 ./nenoform '!(a | b | c | d)' '!a & !b & !c & !d'
 
 # Nested rewritings
-./nenoform '!(a U (!b U ((a & b & c) R d)))' '!a R (b R ((!a | !b | !c) U !d))'
-./nenoform '!(GF a => FG b)' 'GFa & GF!b'
+run 0 ./nenoform '!(a U (!b U ((a & b & c) R d)))' '!a R (b R ((!a | !b | !c) U !d))'
+run 0 ./nenoform '!(GF a => FG b)' 'GFa & GF!b'
diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test
index 1ffd1a3fa..41cf58988 100755
--- a/src/ltltest/parse.test
+++ b/src/ltltest/parse.test
@@ -80,7 +80,7 @@ do
   fi
 
   if test -n "$DOT"; then
-    ./ltl2dot "$f" > parse.dot
+    run 0 ./ltl2dot "$f" > parse.dot
     if $DOT -o /dev/null parse.dot; then
       rm -f parse.dot
     else
@@ -89,4 +89,4 @@ do
       exit 1
     fi
   fi
-done
\ No newline at end of file
+done
diff --git a/src/ltltest/parseerr.test b/src/ltltest/parseerr.test
index b51801b4b..dcb8aa733 100755
--- a/src/ltltest/parseerr.test
+++ b/src/ltltest/parseerr.test
@@ -28,26 +28,21 @@
 
 check()
 {
-  if ./ltl2text "$1" >stdout; then
-    echo "ltl2text unexpectedly parsed '$1' successfully"
-    rm -f stdout
-    exit 1
+  run 1 ./ltl2text "$1" >stdout
+  if test -n "$2"; then
+    echo "$2" >expect
   else
-    if test -n "$2"; then
-      echo "$2" >expect
-    else
-      : >expect
-    fi
-    if cmp stdout expect; then
-      :
-    else
-      echo "'$1' parsed as"
-      cat stdout
-      echo "instead of"
-      cat expect
-      rm -f stdout expect
-      exit 1
-    fi
+    : >expect
+  fi
+  if cmp stdout expect; then
+    :
+  else
+    echo "'$1' parsed as"
+    cat stdout
+    echo "instead of"
+    cat expect
+    rm -f stdout expect
+    exit 1
   fi
 }
 
diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test
index baba86f4c..001e26d4f 100755
--- a/src/ltltest/tostring.test
+++ b/src/ltltest/tostring.test
@@ -27,19 +27,18 @@
 
 set -e 
 
-./tostring 'a'
-./tostring '1'
-./tostring '0'
-./tostring 'a => b'
-./tostring 'G a '
-./tostring 'a U b'
-./tostring 'a & b'
-./tostring 'a & b & c'
-./tostring 'b & a & b'
-./tostring 'b & a & a'
-./tostring 'a & b & (c |(f U g)| e)'
-./tostring 'b & a & a & (c | e |(f U g)| e | c) & b'
-./tostring 'a <=> b'
-./tostring 'a & b & (c |(f U g)| e)'
-./tostring 'b & a & a & (c | e |(g U g)| e | c) & b'
-
+run 0 ./tostring 'a'
+run 0 ./tostring '1'
+run 0 ./tostring '0'
+run 0 ./tostring 'a => b'
+run 0 ./tostring 'G a '
+run 0 ./tostring 'a U b'
+run 0 ./tostring 'a & b'
+run 0 ./tostring 'a & b & c'
+run 0 ./tostring 'b & a & b'
+run 0 ./tostring 'b & a & a'
+run 0 ./tostring 'a & b & (c |(f U g)| e)'
+run 0 ./tostring 'b & a & a & (c | e |(f U g)| e | c) & b'
+run 0 ./tostring 'a <=> b'
+run 0 ./tostring 'a & b & (c |(f U g)| e)'
+run 0 ./tostring 'b & a & a & (c | e |(g U g)| e | c) & b'
diff --git a/src/ltltest/tunabbrev.test b/src/ltltest/tunabbrev.test
index 07dca27fe..5637d8945 100755
--- a/src/ltltest/tunabbrev.test
+++ b/src/ltltest/tunabbrev.test
@@ -28,27 +28,27 @@
 set -e
 
 # A few things that do not change
-./tunabbrev 'a' 'a'
-./tunabbrev '1' '1'
-./tunabbrev '0' '0'
-./tunabbrev 'a U b' 'a U b'
-./tunabbrev 'a & b' 'a & b'
-./tunabbrev 'a & b' 'b & a'
-./tunabbrev 'a & b & c' 'c & a & b'
-./tunabbrev 'a & b & c' 'b & c & a'
-./tunabbrev 'a & b & a' 'b & a & b'
-./tunabbrev 'a & b' 'b & a & b'
-./tunabbrev 'a & b' 'b & a & a'
-./tunabbrev 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
+run 0 ./tunabbrev 'a' 'a'
+run 0 ./tunabbrev '1' '1'
+run 0 ./tunabbrev '0' '0'
+run 0 ./tunabbrev 'a U b' 'a U b'
+run 0 ./tunabbrev 'a & b' 'a & b'
+run 0 ./tunabbrev 'a & b' 'b & a'
+run 0 ./tunabbrev 'a & b & c' 'c & a & b'
+run 0 ./tunabbrev 'a & b & c' 'b & c & a'
+run 0 ./tunabbrev 'a & b & a' 'b & a & b'
+run 0 ./tunabbrev 'a & b' 'b & a & b'
+run 0 ./tunabbrev 'a & b' 'b & a & a'
+run 0 ./tunabbrev 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
 
 # same as in lunabbrev.test:
-./tunabbrev 'a ^ b' '(a & !b) | (!a & b)'
-./tunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
-./tunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
-./tunabbrev '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
+run 0 ./tunabbrev 'a ^ b' '(a & !b) | (!a & b)'
+run 0 ./tunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
+run 0 ./tunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
+run 0 ./tunabbrev '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
 
 # LTL unabbreviations:
-./tunabbrev 'G a ' 'false R a'
-./tunabbrev 'GF a => F G(b)' '!(false R (true U a)) | (true U (false V b))'
-./tunabbrev 'GGGGa' 'false V (false V (false V (false V a)))'
-./tunabbrev 'FFFfalse' 'true U ((true) U (true U (false)))'
+run 0 ./tunabbrev 'G a ' 'false R a'
+run 0 ./tunabbrev 'GF a => F G(b)' '!(false R (true U a)) | (true U (false V b))'
+run 0 ./tunabbrev 'GGGGa' 'false V (false V (false V (false V a)))'
+run 0 ./tunabbrev 'FFFfalse' 'true U ((true) U (true U (false)))'
diff --git a/src/ltltest/tunenoform.test b/src/ltltest/tunenoform.test
index 6f483e23d..e301f24f7 100755
--- a/src/ltltest/tunenoform.test
+++ b/src/ltltest/tunenoform.test
@@ -27,10 +27,10 @@
 
 set -e
 
-./tunenoform '!(a ^ b)' '(a|!b) & (!a|b)'
-./tunenoform '!(a <=> b)' '(a|b) & (!a|!b)'
-./tunenoform '!(a => b)' 'a&!b'
-./tunenoform '!(!a => !b)' '!a&b'
-./tunenoform '!Fa' 'false R !a'
-./tunenoform '!G!a' 'true U a'
-./tunenoform '!(GF a => FG b)' '(0 R (1 U a)) & (0 R (1 U !b))'
+run 0 ./tunenoform '!(a ^ b)' '(a|!b) & (!a|b)'
+run 0 ./tunenoform '!(a <=> b)' '(a|b) & (!a|!b)'
+run 0 ./tunenoform '!(a => b)' 'a&!b'
+run 0 ./tunenoform '!(!a => !b)' '!a&b'
+run 0 ./tunenoform '!Fa' 'false R !a'
+run 0 ./tunenoform '!G!a' 'true U a'
+run 0 ./tunenoform '!(GF a => FG b)' '(0 R (1 U a)) & (0 R (1 U !b))'