diff --git a/_layouts/plugin.html b/_layouts/plugin.html
index e74035afaa513fb1122fa1d230a9d4cc8d67b26e..e88f6f8e397f23a1bde9fc8bdba37d8b57c31742 100644
--- a/_layouts/plugin.html
+++ b/_layouts/plugin.html
@@ -13,7 +13,7 @@ css: plugin
<div>
<a href="/html/kernel-plugin.html"><i class="icon-arrow-left"></i>Back</a>
</div><a class="tabLink active" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
- "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
+ "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/acsl.html">ACSL</a>
</div>
</div>
diff --git a/html/acsl.html b/html/acsl.html
new file mode 100755
index 0000000000000000000000000000000000000000..301e962746422717590df19620e26a17f2e9bc12
--- /dev/null
+++ b/html/acsl.html
@@ -0,0 +1,83 @@
+---
+layout: default
+css: plugin
+title: ACSL
+---
+
+<body class="page-template page-template-page-kernel page-template-page-kernel-php page page-id-179 nonTouch">
+ <div id="wrapper" class="hfeed">
+
+
+ {% include headers.html %}
+
+ <div id="container" class="mainContainer">
+ <div class="tabs">
+ <div class="wrap">
+ <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
+ "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink active" href="/html/acsl.html">ACSL</a>
+ </div>
+ </div>
+
+ <div class="pageKernel pages">
+ <div class="bgTextbig">
+ ACSL
+ </div>
+
+ <div class="wrap">
+ <h1>ANSI/ISO C Specification Language</h1>
+ <p>The ANSI/ISO C Specification Langage (ACSL) is a behavioral
+ specification language for C programs. The design of ACSL is
+ inspired of <a class="extlink" href=
+ "http://www.eecs.ucf.edu/~leavens/JML/index.shtml">JML</a>. It also
+ inherits a lot from the specification language of the source code
+ analyzer <a class="extlink" href=
+ "http://caduceus.lri.fr/">Caduceus</a>, a previous development of
+ one of the partners in the Frama-C project.</p>
+ <p>ACSL can express a wide range of functional properties. The
+ paramount notion in ACSL is the function contract. <span class=
+ "slogan"><a class="pdf" href="download/acsl.pdf">ACSL<br />
+ Reference</a></span> While many software engineering experts
+ advocate the "function contract mindset" when designing complex
+ software, they generally leave the actual expression of the
+ contract to run-time assertions, or to comments in the source code.
+ ACSL is expressly designed for writing the kind of properties that
+ make up a function contract.</p>
+ <p>ACSL is a <em>formal</em> language. This means that the
+ specifications written in ACSL can be automatically manipulated by
+ helper programs, in the same way that a programming language is a
+ formal language manipulated by a compiler, and by opposition to
+ informally written comments that can only be useful to humans.</p>
+ <p>ACSL allows to write contracts that range from the low-level
+ (“<i>this function expects a valid pointer to int</i>â€) to the
+ high-level (“<i>this function expects a nonempty linked list of
+ ints and returns the greatest of these ints</i>â€). It is expressive
+ enough to write complete specifications for many functions, but it
+ can also be used for writing partial specifications. Partial
+ specifications, of which the “<i>expects a valid pointer to
+ int</i>†contract is a typical example, do not describe completely
+ the expected behavior of the function. <span class="slogan">ACSL
+ allows you to write<br />
+ complete specifications.<br />
+ But it does not force you to.</span> Function contracts written as
+ run-time assertions are almost always partial specifications,
+ because a complete specification would be too annoying to write in
+ the same language as the programming language (indeed, most often
+ this would mean programming the function a second time).</p>
+ <p><a href="jessie.html">Jessie</a> and <a href="wp.html">Wp</a>
+ plug-ins use Hoare-style weakest precondition computations to
+ formally prove ACSL properties. The process can be quite automatic,
+ thanks to external theorem provers such as Simplify, or Alt-Ergo,
+ or more interactive, with the use of the Coq proof-assistant. Other
+ plug-ins, such as the <a href="value.html">Eva</a> plug-in, may
+ also contribute to the verification of ACSL properties. They may
+ also report static analysis results in terms of asserted new ACSL
+ properties inside the source code.</p>
+
+ </div>
+ </div>
+ {% include footer.html %}
+
+ <div class="clear"></div>
+ </div>
+ </div>
+</body>
diff --git a/html/gui.html b/html/gui.html
deleted file mode 100755
index d5e870a23e28a7cf1ab4d4e9d43c244e8d6a4750..0000000000000000000000000000000000000000
--- a/html/gui.html
+++ /dev/null
@@ -1,37 +0,0 @@
----
-layout: default
-css: plugin
-title: GUI - Frama-C
----
-
-<body class="page-template page-template-page-kernel page-template-page-kernel-php page page-id-179 nonTouch">
- <div id="wrapper" class="hfeed">
-
-
- {% include headers.html %}
-
- <div id="container" class="mainContainer">
- <div class="tabs">
- <div class="wrap">
- <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
- "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink active" href="/html/gui.html">GUI</a>
- </div>
- </div>
-
- <div class="pageKernel pages">
- <div class="bgTextbig">
- GUI
- </div>
-
- <div class="wrap">
-
- <p> Write something </p>
-
- </div>
- </div>
- {% include footer.html %}
-
- <div class="clear"></div>
- </div>
- </div>
-</body>
diff --git a/html/kernel-plugin.html b/html/kernel-plugin.html
index f1c1d8dea9acd0ad21b899274a0c183caadeda6d..b245c7e1800f15380aa4b14440e76bdea1c93001 100755
--- a/html/kernel-plugin.html
+++ b/html/kernel-plugin.html
@@ -13,7 +13,7 @@ title: Kernel & Plugins - Frama-C
<div class="tabs">
<div class="wrap">
<a class="active tabLink" href="kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
- "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
+ "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/acsl.html">ACSL</a>
<div class="tabOptions">
<div class="pluginSearch">
diff --git a/html/kernel.html b/html/kernel.html
index 42061efa3b5684b7c288149d506ba50b931cbca1..027d5a79a99e20b7acb2c4a75655a5685f3a6c5e 100755
--- a/html/kernel.html
+++ b/html/kernel.html
@@ -14,7 +14,7 @@ title: Kernel & Plugins - Frama-C
<div class="tabs">
<div class="wrap">
<a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink active" href=
- "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
+ "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/acsl.html">ACSL</a>
</div>
</div>