diff --git a/iface/ltsmin/README b/iface/ltsmin/README
index c931a4990..cd043a788 100644
--- a/iface/ltsmin/README
+++ b/iface/ltsmin/README
@@ -121,11 +121,11 @@ Usage with Spot
 Examples
 ========
 
-  Using the dve2check program built into this directory, we can verify
+  Using the modelcheck program built into this directory, we can verify
   that the critical section is accessed infinitely often by some
   processes using:
 
-    % ./dve2check beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
+    % ./modelcheck beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
     2239039 unique states visited
     0 strongly connected components in search stack
     11449204 transitions explored
@@ -134,7 +134,7 @@ Examples
 
   Process P_0 can starve, waiting to enter in critical section:
 
-     % ./dve2check beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)'
+     % ./modelcheck beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)'
      2190 unique states visited
      34 strongly connected components in search stack
      4896 transitions explored
@@ -144,7 +144,7 @@ Examples
    Variable pos[1] is not always < 3 (this formula makes no sense, it
    is just to demonstrate the use of double quote).
 
-     % ./dve2check beem-peterson.4.dve '!G("pos[1] < 3")'
+     % ./modelcheck beem-peterson.4.dve '!G("pos[1] < 3")'
      130 unique states visited
      61 strongly connected components in search stack
      132 transitions explored
@@ -158,7 +158,7 @@ than 2^28, it is way faster than -z (which will work for all values).
 
 Activating state compression will often reduce runtime.  Compare:
 
-% ./dve2check -T beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
+% ./modelcheck -T beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
 2239039 unique states visited
 0 strongly connected components in search stack
 11449204 transitions explored
@@ -176,7 +176,7 @@ running emptiness chec |  1222    100.0 |    18    100.0 |  1240    100.0 |   1
 -------------------------------------------------------------------------------
                  TOTAL |  1222    100.0 |    18    100.0 |  1240    100.0 |
 
-% ./dve2check -T -Z beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
+% ./modelcheck -T -Z beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
 2239039 unique states visited
 0 strongly connected components in search stack
 11449204 transitions explored