Documentation pages

dokuwiki/external_plugins.md

----
-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