diff --git a/dokuwiki/publications.md b/dokuwiki/publications.md index 042e72adda37d37747ae9eea151349bae925eaa7..2bacbb4680edf15292879b6df4f2be0240b50d8f 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