From ee5d0eb40306ac7222686980e5c317e618356316 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 7 Nov 2019 15:48:16 +0100
Subject: [PATCH] [publis] Frama-C general, Eva WP, E-ACSL

---
 dokuwiki/publications.md | 567 +++++++++++++++++----------------------
 1 file changed, 241 insertions(+), 326 deletions(-)

diff --git a/dokuwiki/publications.md b/dokuwiki/publications.md
index bd5432b2..45ac7877 100644
--- a/dokuwiki/publications.md
+++ b/dokuwiki/publications.md
@@ -1,344 +1,307 @@
 ---
 layout: clean_page
 ---
-This page is dedicated to publications related to Frama-C. They are
-categorized by plug-ins. Manuals appear first, then founding thesis and
-articles and finally an inexhaustive lists of other relevant articles.
-Each category is sorted by inverse order of date of publication.
-
-Please feel free to update this page with your own knowledge. Add links
-when possible and only if they do respect copyright.
-
+This page is dedicated to publications related to Frama-C. It is not exhaustive,
+  but focuses on foundational papers for Frama-C and some of its plug-ins.
+
 # Frama-C General
 
-#### Frama-C Manuals
+### Manuals
 
-  - Loïc Correnson, Pascal Cuoq, Florent Kirchner, Virgile Prevosto,
-    Armand Puccetti, Julien Signoles and Boris Yakobowski.  
-    **Frama-C User Manual.**  
-    <http://frama-c.com/download/frama-c-user-manual.pdf>.  
+  - Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze,
+  Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski.
+    **Frama-C User Manual.**
+    <http://frama-c.com/download/frama-c-user-manual.pdf>.
     *The manual introducing common features to all analyzers.*
-
 <!-- end list -->
-
-  - Julien Signoles, Loïc Correnson and Virgile Prevosto.  
+      
+  - Julien Signoles, Thibaud Antignac, Loïc Correnson, Matthieu Lemerre,
+  and Virgile Prevosto.  
     **Frama-C Plug-in Development Guide**.  
     <http://frama-c.com/download/frama-c-plugin-development-guide.pdf>.  
     *The manual for developing a Frama-C plug-in.*
-
-#### ACSL manuals
-
-  - Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin
-    Monate, Yannick Moy and Virgile Prevosto.  
-    **ACSL: ANSI/ISO C Specification Language. Version 1.7**.  
+ <!-- end list -->
+
+   - Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin
+   Monate, Yannick Moy, and Virgile Prevosto.  
+    **ACSL: ANSI/ISO C Specification Language.**.  
     <http://frama-c.com/download/acsl.pdf>.  
     *The reference manual of ACSL, the specification language used by
     Frama-C.*
-
-<!-- end list -->
-
-  - Virgile Prevosto.  
-    **ACSL Tutorial.**  
-    <http://frama-c.com/download/acsl-tutorial.pdf>.  
-    *The official tutorial of ACSL.*
-
-<!-- end list -->
-
-  - Jochen Burghardt and Jens Gerlach.  
-    **ACSL by Example**. *A fairly complete tour of ACSL and WP features
-    through various functions inspired from C++ STL.*
-      - <https://github.com/fraunhoferfokus/acsl-by-example> (Major
-        version of the document corresponds to the Frama-C version that
-        has been used to make the proofs).
-
 <!-- end list -->
 
-  - Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude
-    Marché, Benjamin Monate, Yannick Moy and Virgile Prevosto.  
-    **ACSL version 1.7. Implementation in Fluorine-20130601**.  
-    <http://frama-c.com/download/acsl-implementation-Fluorine-20130601.pdf>.  
-    *The sub-part of ACSL implemented in the latest Frama-C release.*
+### Founding Articles
 
-#### Founding Articles
-
-  - Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien
-    Signoles and Boris Yakobowski.  
+  - Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles,
+    and Boris Yakobowski.  
     **Frama-C, A Software Analysis Perspective.**  
     In Formal Aspects of Computing, vol. 27 issue 3, March 2015.  
     <http://dx.doi.org/10.1007/s00165-014-0326-7>.  
     Extended version of the following paper.
-
 <!-- end list -->
-
+
   - Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto,
-    Julien Signoles and Boris Yakobowski.  
+    Julien Signoles, and Boris Yakobowski.  
     **Frama-C, A Software Analysis Perspective.**  
     In proceedings of International Conference on Software Engineering
-    and Formal Methods 2012 (SEFM'12), October 2012.  
+    and Formal Methods 2012 (SEFM), October 2012.  
     *This paper presents a synthetic view of Frama-C, its main and
     composite analyses, and some of its industrial achievements.*
-
 <!-- end list -->
-
-  - Loïc Correnson and Julien Signoles.  
+
+#### Articles about the Frama-C Kernel
+
+  - Julien Signoles.
+    **Software Architecture of Code Analysis Frameworks Matters:
+     The Frama-C Example.**
+    In Formal Integrated Development Environment (F-IDE), June 2015.
+    <http://julien.signoles.free.fr/publis/2015_fide.pdf>
+      *This papers presents the Frama-C architecture and discusses its design
+    choices.*
+<!-- end list -->
+
+  - Loïc Correnson, and Julien Signoles.  
     **Combining Analyses for C Program Verification.**  
     In proceedings of International Workshop on Formal Methods for
-    Industrial Critical Systems 2012 (FMICS'12), August 2012.  
+    Industrial Critical Systems 2012 (FMICS), August 2012.  
+    <http://julien.signoles.free.fr/publis/2012_fmics.pdf>
     *This paper explains how Frama-C combines several partial results
     coming from its plug-ins into a fully consolidated validity status
     for each program property.*
-
-<!-- end list -->
-
-  - Pascal Cuoq, Damien Doligez, Julien Signoles.  
-    **Lightweight Typed Customizable Unmarshaling.** ML workshop 2011
-    <http://blog.frama-c.com/public/unmarshal.pdf>.
-
-<!-- end list -->
-
-  - Julien Signoles.  
-    **Une bibliothèque de typage dynamique en OCaml.**  
-    In Hermann, editor, JFLA 11, Actes des Journées Francophones des
-    Langages Applicatifs 2011, January 2011. In French.  
-    *Cet article présente une bibliothèque OCaml fournissant une
-    représentation dynamique des types monomorphes, y compris pour les
-    instances des types polymorphes et les types de données abstraits.
-    Elle permet ainsi de voir les types OCaml comme des citoyens de
-    première classe. Elle comble aussi le fossé séparant OCaml des
-    langages dynamiques en mêlant vérifications statiques et dynamiques
-    des types. Nous nous concentrons ici sur le coeur de son
-    implantation, ses propriétés théoriques et l'usage qui en est fait
-    dans Frama-C, plateforme logicielle libre d'analyse statique de
-    programmes C au sein de laquelle cette bibliothèque est distribuée.*
-
+<!-- end list -->
+
+  - Pascal Cuoq, Damien Doligez, and Julien Signoles.  
+    **Lightweight Typed Customizable Unmarshaling.**
+    In Workshop on ML, September 2011.
+    <http://blog.frama-c.com/public/unmarshal.pdf>.
+    *This short paper presents how Frama-C unmarshal its data.*
 <!-- end list -->
 
-  - Pascal Cuoq and Julien Signoles.  
+  - Pascal Cuoq, Julien Signoles, Patrick Baudin, Richard Bonichon,
+    Géraud Canet, Loïc Correnson, Benjamin Monate, Virgile Prevosto, and
+    Armand Puccetti.
     **Experience Report: OCaml for an Industrial-Strength Static
     Analysis Framework.**  
-    In Proceedings of International Conference of Functional Programming
-    (ICFP'09), pages 281--286, September 2009.  
+    In International Conference of Functional Programming (ICFP),
+    September 2009.  
+    <http://julien.signoles.free.fr/publis/2009_icfp.pdf>
     *This experience report describes the choice of OCaml as the
-    implementation language for Frama-C, a framework for the static
-    analysis of C programs. OCaml became the implementation language for
-    Frama-C because it is expressive. Most of the reasons listed in the
-    remaining of this article are secondary reasons, features which are
-    not specific to OCaml (modularity, availability of a C parser,
-    control over the use of resources...) but could have prevented the
-    use of OCaml for this project if they had been missing.*
-
+    implementation language for Frama-C.*
 <!-- end list -->
-
+
+  - Julien Signoles.
+    **Comment un chameau peut-il écrire un journal?**
+    In Journées Francophones des Langages Applicatifs (JFLA), January 2014.
+    In French.
+    *Presentation of the journalization mechanism of Frama-C.*
+<!-- end list -->
+
   - Julien Signoles.  
+    **Une bibliothèque de typage dynamique en OCaml.**  
+    In Journées Francophones des Langages Applicatifs (JFLA), January 2011.
+    In French.  
+    *Presentation of the Frama-C library for dynamic typing and its usage.*
+<!-- end list -->
+
+  - Julien Signoles.
     **Foncteurs impératifs et composés: la notion de projets dans
-    Frama-C.**  
-    In Hermann, editor, JFLA 09, Actes des vingtièmes Journées
-    Francophones des Langages Applicatifs 2009, volume 7.2 of Studia
-    Informatica Universalis, pages 245--280, June 2009. In French.  
-    *Cet article présente la bibliothèque de projets de Frama-C, une
-    plateforme facilitant le développement d'analyseurs statiques de
-    programmes C. Grâce à sa description, nous présentons une
-    utilisation originale des foncteurs du système de modules de ML qui
-    exploite aussi bien leur caractère impératif que compositionnel.
-    Ceci est le seul véritable recours pour réaliser la fonctionalité
-    souhaitée de manière bien typée. En outre, nous montrons un exemple
-    peu fréquent d'un même foncteur appliqué plusieurs centaines de
-    fois. Cet article introduit aussi la plateforme Frama-C elle-même, à
-    travers un de ses aspects essentiels, la notion de projet.*
-
-#### Other Articles
-
-  - Dillon Pariente and Emmanuel Ledinot.  
-    **Formal Verification of Industrial C Code using Frama-C: a Case
-    Study.**  
-    In Proceedings of First International Conference on Formal
-    Verification of Object-Oriented Software (FoVeOOS'10), June 2010.  
-    *This paper gives some results and lessons learnt with Frama-C, a
-    static analysis toolbox, used to prove behavioral and safety
-    properties on an industrial code. After a short presentation of the
-    methods and tools background, the related industrial use case is
-    briefly exposed, with an overview of the process that was followed.
-    Then the positive results obtained so far are presented, with a few
-    practices and additional tools developed in-house. To conclude, this
-    paper presents some needs and future work directions that should be
-    addressed, to ensure a technology readiness level compliant with
-    operational use of formal verification into an industrial
-    development environment.*  
-    **See also the [associated video](http://frama-c.com/video.html)**.
-
-<!-- end list -->
-
-  - Matti Mantere, Ilkka Uusitalo, Juha Röning.  
-    **Comparison of Static Code Analysis Tools.**  
-    securware, Third International Conference on Emerging Security
-    Information, Systems and Technologies, pages 15--22, June 2009.  
-    *In this paper we compare three static code analysis tools. The
-    tools represent three different approaches in the field of static
-    analysis: Fortify SCA is a non-annotation based heuristic analyzer,
-    Splint represents an annotation based heuristic analyzer, and
-    Frama-C an annotation based correct analyzer. The tools are compared
-    by analysing their performance when checking a demonstration code
-    with intentionally implemented errors.*
-
-# Eva / Value Analysis
-
-#### Manual
-
-  - Pascal Cuoq and Virgile Prevosto.  
-    **Frama-C’s value analysis plug-in.**  
-    <http://frama-c.com/download/frama-c-value-analysis.pdf>.  
-    *The official manual for the value analysis of Frama-C.*
-
-#### Founding Articles
+    Frama-C.**
+    In Journées Francophones des Langages Applicatifs (JFLA), January 2009.
+    In French.  
+    *Presentation of the Frama-C library providing its notion of
+     projects.*
+<!-- end list -->
+
+### Tutorials
+
+  - Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue.
+    **A Lesson on Verification of IoT Software with Frama-C.**
+    In International Conference on High Performance Computing & Simulation
+    (HPCS), July 2018.
+    <https://hal.inria.fr/hal-02317078>
+<!-- end list -->
+      
+  - Nikolai Kosmatov and Julien Signoles.
+    **Frama-C, a Collaborative Framework for C Code Verification.
+      Tutorial Synopsis.**
+    In International Conference on Runtime Verification (RV 2016),
+    September 2016.
+    <http://julien.signoles.free.fr/publis/2016_rv.pdf>
+<!-- end list -->
+
+# Eva
+
+### Manual
+
+  - David Bühler, Pascal Cuoq, Boris Yakobowski, Matthieu Lemerre,
+      André Maroneze, Valentin Perelle, and Virgile Prevosto.
+    **Eva - The Evolved Value Analysis plug-in.**  
+    <http://frama-c.com/download/frama-c-eva-manual.pdf>.
+<!-- end list -->
+
+### Thesis
+
+  - David Bühler.
+    **EVA, an Evolved Value Analysis for Frama-C: structuring an abstract
+    interpreter through value and state abstractions.**
+    PhD Thesis, University of Rennes 1, March 2017.
+    <http://http://www.theses.fr/2017REN1S016>
+      
+### Founding Articles
 
   - Sandrine Blazy, David Bühler, and Boris Yakobowski.  
     **Structuring Abstract Interpreters through State and Value
-    Abstractions**  
-    To be published in the proceedings of VMCAI 2017. [local
-    version](/assets/dokuwiki/articles/eva-vmcai2017.pdf)  
-    *The formalization of the communication mechanism between
+    Abstractions**
+    In International Conference on Verification, Model Checking, and Abstract
+    Interpretation (VMCAI), January 2017.
+    <https://hal-cea.archives-ouvertes.fr/cea-01808886>
+    *Formalization of the communication mechanism between
     abstractions in EVA.*
-
-<!-- end list -->
-
-  - Richard Bonichon and Pascal Cuoq.  
-    **A Mergeable Interval Map.**  
-    In Studia Informatica Universalis, vol. 9, nb. 1. pp. 5--37. 2011  
-    <http://studia.complexica.net/index.php?option=com_content&view=article&id=185%3Aa-mergeable-interval-map%20pp-5-37&catid=56%3Anumber-1&Itemid=100&lang=en>  
-    Extended version of the paper below.
-
-<!-- end list -->
-
-  - Richard Bonichon and Pascal Cuoq.  
-    **Une table d'association d'intervalles fusionnable.**  
-    In Proceedings of vingt-et-unième Journées Francophones des Langages
-    Applicatifs (JFLA'10). February 2010. The body of the article is in
-    English.
-
-<!-- end list -->
-
+<!-- end list -->
+
+  - Richard Bonichon and Pascal Cuoq.
+    **A Mergeable Interval Map.**
+    In  Journées Francophones des Langages Applicatifs (JFLA), January 2011.
+    <http://studia.complexica.net/index.php?option=com_content&view=article&id=185%3Aa-mergeable-interval-map%20pp-5-37&catid=56%3Anumber-1&Itemid=100&lang=en>
+    *Presentation of one of the most important internal datastructure of Eva.*
+<!-- end list -->
+
+### Other Articles
+
   - Géraud Canet, Pascal Cuoq and Benjamin Monate.  
     **A Value Analysis for C Programs.**  
     In Proceedings of the Ninth IEEE International Working Conference on
-    Source Code Analysis and Manipulation (SCAM'09). September 2009.  
-    *We demonstrate the value analysis of Frama-C. Frama-C is an Open
-    Source static analysis framework for the C language. In Frama-C,
-    each static analysis technique, approach or idea can be implemented
-    as a new plug-in, with the opportunity to obtain information from
-    other plug-ins, and to leave the verification of difficult
-    properties to yet other plug-ins. The new analysis may in turn
-    provide access to the data it has computed. The value analysis of
-    Frama-C is a plug-in based on abstract interpretation. It computes
-    and stores supersets of possible values for all the variables at
-    each statement of the analyzed program. It handles pointers, arrays,
-    structs, and heterogeneous pointer casts. Besides producing
-    supersets of possible values for the variables at each point of the
-    execution, the value analysis produces run-time-error alarms. An
-    alarm is emitted for each operation in the analyzed program where
-    the value analysis cannot guarantee that there will not be a
-    run-time error.*
-
-<!-- end list -->
-
+    Source Code Analysis and Manipulation (SCAM). September 2009.
+    *Presentation of a former version of Eva.*
+<!-- end list -->
+
   - Pascal Cuoq and Damien Doligez.  
     **Hashconsing in an incrementally garbage-collected system: a story
     of weak pointers and hashconsing in OCaml 3.10.2.**  
-    In Proceedings of the 2008 ACM SIGPLAN Workshop on ML (ML'08), pages
-    13--22, September 2008.  
-    *This article describes the implementations of weak pointers, weak
-    hashtables and hashconsing in version 3.10.2 of the Objective Caml
-    system, with focus on several performance pitfalls and their
-    solutions.*
-
-#### Other Articles
-
-  - Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John
-    Regehr, Boris Yakobowski and Xuejun Yang.  
-    **Testing Static Analyzers with Randomly Generated Programs.**  
-    In Proceedings of the 4th NASA Formal Methods Symposium (NFM 2012),
-    LNCS 7226, April 2012.
-
-<!-- end list -->
+    In Workshop on ML, September 2008.
+    *This article describes weak pointers, weak hashtables and hashconsing as
+    implemented in OCaml and used in a former version of Eva.*
+<!-- end list -->
+
+# WP
 
-  - Pascal Cuoq, Philippe Hilsenkopf, Florent Kirchner, Sébastien Labbé,
-    Nguyen Thuy and Boris Yakobowski.  
-    **Formal verification of software important to safety using the
-    Frama-C tool suite.**  
-    NPIC\&HMIT 2012.
+### Manual
 
+  - Patrick Baudin, François Bobot, Loïc Correnson, and Zaynah Dargaye.  
+    **WP Plug-in Manual.**  
+    <http://frama-c.com/download/frama-c-wp-manual.pdf>.  
+    *The official manual for the WP plug-in.*
 <!-- end list -->
-
-  - Chatzieleftheriou, G. and Katsaros, P.  
-    **Test driving static analysis tools in search of C code
-    vulnerabilities.**  
-    In Proceedings of the 6th IEEE International Workshop on Security,
-    Trust, and Privacy for Software Applications (STPSA'11), Munich,
-    Germany, IEEE Computer Society, 2011.
-
+
+### Founding Articles
+
+  - Loïc Correnson.
+    **Qed. Computing What Remains to Be Proved.**
+    In NASA Formal Methods (NFM), April 2012.
+    *Presentation of Qed, a core library of WP that simplifies proof obligations
+    before sending them to provers.*
+<!-- end list -->
+      
+### Tutorials
+
+  - Allan Blanchard.
+    ** Introduction to C Program Proof with Frama-C and its WP plug-in.**
+    <https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en>
 <!-- end list -->
-
-  - Armand Puccetti.  
-    **Static Analysis of the XEN Kernel using Frama-C.**  
-    Journal of Universal Computer Science, volume 16, issue 4, 2010.  
-    *In this paper, we describe the static analysis of the XEN 3.0.3
-    hypervisor using the Frama-C static analysis tool.*
-
+     
+  - Jochen Burghardt and Jens Gerlach.  
+    **ACSL by Example**.
+    <https://github.com/fraunhoferfokus/acsl-by-example>
+    *A fairly complete tour of ACSL and WP features through various functions
+      inspired from C++ STL.*
 <!-- end list -->
-
-  - Pascal Berthomé, Karinne Heydemann, Xavier Kauffmann-Tourkestansky
-    and Jean-François Lalande.  
-    **Attack model for verification of interval security properties for
-    smart card C codes.**  
-    Proceedings of the 5th Workshop on Programming Languages and
-    Analysis for Security (PLAS'10). 2010.  
-    *Smart card programs are subject to physical attacks that disturb
-    the execution of the embedded code. These attacks enable attackers
-    to steal valuable information or to force a malicious behavior upon
-    the attacked code. This paper proposes a methodology to check
-    interval security properties on smart card source codes. The goal is
-    to identify critical attacks that violate these security properties.
-    The verification takes place at source-level and considers all
-    possible attacks thanks to a proposed source-level model of physical
-    attacks. The paper defines an equivalence relation between attacks
-    and shows that a code can be divided into areas where attacks are
-    equivalent. Thus, verifying an interval security property
-    considering all the possible attacks requires to verify as many
-    codes as the number of equivalence classes. This paper provides a
-    reduction algorithm to define the classes i.e. the minimal number of
-    attacked codes that covers all possible attacks. The paper also
-    proposes a solution to make the property verification possible for
-    large codes or codes having unknown source parts.*
-
-# WP
-
-#### Manual
-
-  - Loïc Correnson and Zaynah Dargaye and Anne Pacalet.  
-    **WP (Draft) Manual.**  
-    <http://frama-c.com/download/frama-c-wp-manual.pdf>.  
-    *A draft manual for the WP plug-in.*
-
+
 #### Other articles
 
   - Pascal Cuoq, Benjamin Monate, Anne Pacalet and Virgile Prevosto.  
-    **Functional Dependencies of C Functions via Weakest
-    Pre-Conditions**  
-    International Journal on Software Tools for Technology Transfer
-    (STTT), edition VSTTE 2009-2010,
+    **Functional Dependencies of C Functions via Weakest Pre-Conditions**
+    In International Journal on Software Tools for Technology Transfer
+    (STTT), 2010,
     [SpringerLink](http://www.springerlink.com/content/yj344380377p4011/)  
     [More information](functional_dependencies)
+<!-- end list -->
+
+# E-ACSL
+
+### Manual
 
+  - Julien Signoles and Kostyantyn Vorobyov.  
+    **E-ACSL User Manual.**
+    <http://frama-c.com/download/e-acsl/e-acsl-manual.pdf>.  
+    *The official manual of the Frama-C plug-in E-ACSL.*
 <!-- end list -->
-
-  - Arnaud Dieumegard and Marc Pantel.  
-    **Vérification d’un générateur de code par génération
-    d’annotations.**  
-    Conférence en IngénieriE du Logiciel (CIEL), Juin 2012.  
-    <http://gpl2012.irisa.fr/sites/default/files/CIEL2012-Dieumegard-paper34.pdf>
-  - Allan Blanchard.  
-    **Introduction to C Program Proof using Frama-C and its WP Plugin.**  
-    WP tutorial, available at <http://allan-blanchard.fr/teaching.html>.
-
+
+  - Julien Signoles.  
+    **E-ACSL: Executable ANSI/ISO C Specification Language.**
+    <http://frama-c.com/download/e-acsl/e-acsl.pdf>.  
+    *The reference manual of the E-ACSL specification language.*
+<!-- end list -->
+
+### Thesis
+
+  - Julien Signoles.
+    **From Static Analysis to Runtime Verification with Frama-C and E-ACSL.**
+    Habilitation Thesis, University of Paris Sud, July 2018.
+     <http://julien.signoles.free.fr/publis/hdr.pdf>
+<!-- end list -->
+
+#### Founding Articles
+
+  - Julien Signoles, Nikolai Kosmatov, and Kostyantyn Vorobyov.
+  **E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs.
+  Tool Paper.**
+  In International Workshop on Competitions, Usability, Benchmarks, Evaluation,
+  and Standardisation for Runtime Verification Tools (RV-CuBES), September 2017.
+  <http://julien.signoles.free.fr/publis/2017_rvcubes_tool.pdf>
+  *An overview of the E-ACSL plug-in.*
+<!-- end list -->
+
+  - Kostyantyn Vorobyov, Julien Signoles, and Nikolai Kosmatov.
+    Shadow state encoding for efficient monitoring of block-level properties.
+    In International Symposium on Memory Management (ISMM), June 2017.
+    <http://julien.signoles.free.fr/publis/2017_ismm.pdf>
+    *Presentation of the shadow memory technique used by E-ACSL to monitor
+      memory properties.*
+<!-- end list -->
+    
+  - Mickaël Delahaye, Nikolaï Kosmatov and Julien Signoles.  
+    **Common Specification Language for Static and Dynamic Analysis of C
+    Programs.**  
+    In Proceedings of Symposium on Applied Computing 2013 (SAC), March 2013.
+    <http://kosmatov.perso.sfr.fr/nikolai/publications/delahaye_ks_sac_2013.pdf>
+    *An overview of the specification language.*
+<!-- end list -->
+
+#### Other Articles
+
+  - Kostyantyn Vorobyov, Nikolai Kosmatov, and Julien Signoles.
+    **Detection of Security Vulnerabilities in C Code using Runtime
+    Verification.**
+    In International Conference on Tests and Proofs (TAP), June 2018.
+    <http://julien.signoles.free.fr/publis/2018_tap_vorobyov.pdf>
+    *Explore how some runtime verification tools (including E-ACSL) may detect
+     security vulnerabilities.*
+<!-- end list -->
+
+  - Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles, and Arvid Jakobsson.
+    **Runtime detection of temporal memory errors.**
+    In International Conference on Runtime Verification (RV), September 2017.
+    <http://julien.signoles.free.fr/publis/2017_rv.pdf>
+<!-- end list -->
+
+  - Nikolaï Kosmatov, Guillaume Petiot and Julien Signoles.
+    **An Optimized Memory Monitoring for Runtime Assertion Checking of C
+    Programs.** 
+    In Proceedings of Runtime Verification 2013 (RV), September 2013.
+    *Presentation of the runtime memory model used by a former version of
+     E-ACSL.*
+<!-- end list -->
+
 # Jessie
 
 #### Manual
@@ -616,54 +579,6 @@ detecting loss of separation among aircraft.*
     showing the use of Aoraï in generating a threat scenario in a
     driver.
 
-# E-ACSL
-
-#### Manual
-
-  - Julien Signoles.  
-    **E-ACSL User Manual.**  
-    <http://frama-c.com/download/e-acsl/e-acsl-manual.pdf>.  
-    *The official manual of the Frama-C plug-in E-ACSL.*
-
-<!-- end list -->
-
-  - Julien Signoles.  
-    **E-ACSL: Executable ANSI/ISO C Specification Language. Version
-    1.7.**  
-    <http://frama-c.com/download/e-acsl/e-acsl.pdf>.  
-    *The reference manual of the E-ACSL specification language.*
-
-<!-- end list -->
-
-  - Julien Signoles.  
-    **E-ACSL Version 1.7. Implementation in Frama-C Plug-in E-ACSL
-    version 0.3.**  
-    <http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf>.  
-    *What part of the E-ACSL specification language is currently
-    implemented in the E-ACSL plug-in.*
-
-#### Founding Articles
-
-  - Mickaël Delahaye, Nikolaï Kosmatov and Julien Signoles.  
-    **Common Specification Language for Static and Dynamic Analysis of C
-    Programs.**  
-    In Proceedings of Symposium on Applied Computing 2013 (SAC'13),
-    March 2013.  
-    <http://kosmatov.perso.sfr.fr/nikolai/publications/delahaye_ks_sac_2013.pdf>.
-
-<!-- end list -->
-
-  - Nikolaï Kosmatov, Guillaume Petiot and Julien Signoles.  
-    **An Optimized Memory Monitoring for Runtime Assertion Checking of C
-    Programs.**  
-    In Proceedings of Runtime Verification 2013 (RV'13), September 2013.
-
-#### Other Article
-
-  - Nikolaï Kosmatov and Julien Signoles.  
-    **A Lesson on Runtime Assertion Checking with Frama-C. RV 2013
-    Tutorial.**  
-    In Proceedings of Runtime Verification 2013 (RV'13), September 2013.
 
 # Security Slicing
 
-- 
GitLab