Commit de83f8cc authored by Allan Blanchard's avatar Allan Blanchard
Browse files

RPP + MetACSL + E-ACSL

parent 443ef2bf
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment