X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=2020-frama-c%2F9200-alternatives.html;fp=2020-frama-c%2F9200-alternatives.html;h=f594042ad315cead1862eb24a191878ba64ccaca;hb=6d2dcd916aa3e435d1f8ce691127bd891fc3c69a;hp=2469692d61a45d9d6f2166bbfc7905ce22068003;hpb=a44fc27c4a4b02ed570dd5567ff8d309b885e904;p=libguestfs-talks.git

diff --git a/2020-frama-c/9200-alternatives.html b/2020-frama-c/9200-alternatives.html
index 2469692..f594042 100644
--- 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).