AnaStaSec: publications related to the project
|
Static Analysis for Security Properties.
Publications related to the project
-
Frédéric Besson.
A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data.
J. Autom Reasoning 62(4), 2019.
- Frédéric Besson, Sandrine Blazy, Pierre Wilke.
CompCerts: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics.
J. Autom Reasoning 63(2), (2019)
-
Mounir Assaf.
From Qualitative to Quantitative Program Analysis : Permissive Enforcement of Secure Information Flow.
PhD thesis. Rennes, France. May 2015.
- Frédéric Besson, Sandrine Blazy, Pierre Wilke.
A Concrete Memory Model for CompCert.
ITP 2015: 67-83, 2015. - Gergö Barany.
Hybrid Information Flow Analysis for Programs with Arrays.
Workshop on Verification and Program Transformation.
January 2016 - Mounir Assaf, Julien Signoles, Eric Totel, Frederic Tronel.
The Cardinal Abstraction for Quantitative Information Flow.
Workshop on Foundations of Computer Security 2016.
June 2016. - Mounir Assaf, David Naumann, Julien Signoles, Éric Totel, Fréd´ric Tronel.
Hypercollecting Semantics and its Application to Static Analysis of Information Flow.
POPL 2017: 2017. - Bruno Blanchet.
Symbolic and Computational Mechanized Verification of the (ARINC823) Avionic Protocols.
CSF 2017: 2017 - Frédéric Besson, Sandrine Blazy, Pierre Wilke.
Compcerts: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics.
ITP 2017, Springer. - Gergö Barany and Julien Signoles.
Hybrid Information Flow Analysis for Real-World C Code.
International Conference on Tests and Proofs (TAP 2017). July 2017. - Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles and Arvid Jakobsson.
Runtime Detection of Temporal Memory Errors.
International Conference on Runtime Verification (RV 2017). September 2017. - Frédéric Besson, Thomas, P. Jensen, Julien Lepiller.
Modular Software Fault Isolation as Abstract Interpretation.
Static Analysis Symposium (SAS 2018), August 2018. - Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas, P. Jensen, Pierre Wilke.
Compiling Sandboxes: Formally Verified Software Fault Isolation.
European Symposium on Programing (ESOP 2019), April 2019, Springer. - Benjamin Lipp, Bruno Blanchet, and Karthikeyan Bhargavan.
A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol.
In IEEE European Symposium on Security and Privacy (EuroS&P 2019), pages 231-246, Stockholm, Sweden, June 2019. - Marc Chevalier, Jérôme Feret. Verification.
Sharing Ghost Variables in a Collection of Abstract Domains.
Model Checking, and Abstract Interpretation (VMCAI 2020), January 2020, - Pascal Cuoq, Raphaël Rieu-Helft.
Result graphs for an abstract interpretation-based static analyzer.
JFLA 2017 - Julien Signoles.
Quand une machine arrive à comprendre une machine : l'analyse formelle de code.
Nuits des Sciences et des Lettres.
École Normale Supérieure. Juin 2016.
