Reworking after run through with Paolo.

[libguestfs-talks.git] / 2020-frama-c / 9200-alternatives.html

diff --git a/2020-frama-c/9200-alternatives.html b/2020-frama-c/9200-alternatives.html
index 2469692..f594042 100644 (file)
--- a/2020-frama-c/9200-alternatives.html
+++ b/2020-frama-c/9200-alternatives.html
@@ -9,8 +9,11 @@
   is a formally verified subset of the Ada programming language
   (tagline: <i>"You simply can't write better code"</i>).
 
-<li> <a href="http://klee.github.io/">KLEE</a> has similarities
-  but is not a formal proof system.
+<li> <a href="https://lamport.azurewebsites.net/tla/tla.html">TLA+</a>
+  is useful for proving distributed systems over time.
+
+<li> <a href="http://why3.lri.fr">Why3 / WhyML</a>
+  can be used for constructive proofs.
 
 <li> <a href="http://compcert.inria.fr/">CompCert</a>
   is INRIA's verified C compiler (not open source).