From de83f8ccc10a945293c3965d87f4b612a9a49e72 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 7 Aug 2020 17:13:14 +0200
Subject: [PATCH] RPP + MetACSL + E-ACSL

---
 dokuwiki/publications.md | 43 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 42 insertions(+), 1 deletion(-)

diff --git a/dokuwiki/publications.md b/dokuwiki/publications.md
index 042e72ad..2bacbb46 100644
--- a/dokuwiki/publications.md
+++ b/dokuwiki/publications.md
@@ -246,6 +246,15 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
     In Proceedings of Runtime Verification 2013 (RV), September 2013.\
     *Presentation of the runtime memory model used by a former version of
      E-ACSL.*
+  - Dara Ly, Nikolai Kosmatov, Julien Signoles and Frédéric Loulergue.\
+    **Soundness of a Dataflow Analysis for Memory Monitoring.**\
+    In Workshop on Languages and Tools for Ensuring Cyber-Resilience in
+    Critical Software-Intensive Systems (HILT) , November 2018.\
+    <https://hal.archives-ouvertes.fr/cea-02283406/>
+  - Dara Ly, Nikolai Kosmatov, Frédéric Loulergue and Julien Signoles.\
+    **Verified Runtime Assertion Checking for Memory Properties.**\
+    In International Conference on Tests and Proofs (TAP), June 2020.\
+    <https://hal-cea.archives-ouvertes.fr/cea-02879211>
 
 # Aoraï
 
@@ -297,7 +306,15 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
     Pascale Le Gall.\
     **MetAcsl: Specification and Verification of High-Level Properties.**\
     In International Conference on Tools and Algorithms for the Construction
-    and Analysis of Systems (TACAS), April 2019.
+    and Analysis of Systems (TACAS), April 2019.\
+    <https://hal-cea.archives-ouvertes.fr/cea-02019790>
+
+  - Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling and
+    Pascale Le Gall.\
+    **Tame Your Annotations with MetAcsl: Specifying, Testing and Proving
+    High-Level Properties.**\
+    In Tests and Proofs (TAP), 13th International Conference, October 2019.\
+    <https://hal.archives-ouvertes.fr/cea-02301892/>
 
 ### PathCrawler
 
@@ -401,6 +418,30 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
     The final publication is available from IEEE.\
     <http://dx.doi.org/10.1109/ICSTW.2011.85>
 
+
+### RPP
+
+##### Founding Articles
+
+  - Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall and Virgile Prevosto.\
+    **RPP: Automatic Proof of Relational Properties by Self-composition.**\
+    In Tools and Algorithms for the Construction and Analysis of Systems
+    23rd International Conference, {TACAS} 2017.\
+    <https://hal-cea.archives-ouvertes.fr/cea-01808885>
+  - Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto and
+    Guillaume Petiot.\
+    **Static and Dynamic Verification of Relational Properties on
+    Self-composed C Code.**\
+    In Tests and Proofs - 12th International Conference, TAP@STAF 2018.\
+    <https://hal-cea.archives-ouvertes.fr/cea-01835470>
+    
+##### Thesis
+
+  - Lionel Blatter.\
+    **Relational properties for specification and verification of C programs in Frama-C.**\
+    PhD Thesis, University of Paris Saclay, December 2019.\
+    <http://http://www.theses.fr/2017REN1S016>
+
 ### SecureFlow
 
 ##### Thesis
-- 
GitLab