From e4e7962c728607207887f4f4399181bf5a3baabc Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 7 Nov 2019 16:30:24 +0100
Subject: [PATCH] External plugins (update dead links + new external plugins)

---
 dokuwiki/external_plugins.md | 29 +++++++++++++++++++++++++----
 1 file changed, 25 insertions(+), 4 deletions(-)

diff --git a/dokuwiki/external_plugins.md b/dokuwiki/external_plugins.md
index 4ee34c09..28429e77 100644
--- a/dokuwiki/external_plugins.md
+++ b/dokuwiki/external_plugins.md
@@ -1,6 +1,6 @@
----
-layout: clean_page
----
+---
+layout: clean_page
+---
 # External plug-ins
 
 This is a list of plug-ins that you may find useful but are not
@@ -12,6 +12,27 @@ luck on the mailing list.
 Add your own plug-in if you think it can be useful to other and want to
 share it with the world\!
 
+## Pilat
+
+URL: <http://steven-de-oliveira.fr/index.php?page=tool_pilat>
+
+PILAT (for Polynomial Invariants by Linear Algebra Tool) is an invariant
+generator based on the study of matrices. It processes loops with polynomial
+assignments and linearize them, then searches for left eigenvectors of the
+resulting matrix. Those vectors expresses invariants of the loop.
+
+## StaDy
+
+URL: <https://github.com/gpetiot/Frama-C-StaDy>
+
+StaDy is an integration of the concolic test generator PathCrawler within
+the software analysis platform Frama- C. When executing a dynamic analysis
+of a C code, the integrated test generator also exploits its formal specification,
+written in an executable fragment of the acsl specification language shared
+with other analyzers of Frama-C. The test generator provides the user with
+accurate verdicts, that other Frama-C plugins can reuse to improve their own
+analyses.
+
 ## Jessie
 
 URL: <http://krakatoa.lri.fr/>
@@ -30,7 +51,7 @@ asked about it have been gathered on their [own page](/dokuwiki/jessie.html), or
 
 ## Celia
 
-URL: <http://www.liafa.univ-paris-diderot.fr/celia/>
+URL: <https://www.irif.fr/~sighirea/celia/>
 
 CELIA is a tool for the static analysis and verification of C programs
 manipulating dynamic (singly linked) lists. The static analyser computes
-- 
GitLab