Verified Software Toolchain, Programming Languages and Systems (ESOP), vol.6602, pp.1-17, 2011. ,
Verification of a Cryptographic Primitive, p.256, 2015. ,
, ACM Trans. Program. Lang. Syst, vol.37, issue.7, pp.1-7, 2015.
Program Logics for Certified Compilers, 2014. ,
, ACSL: ANSI/ISO C Specification Language, 2018.
Interactive Theorem Proving and Program Development, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C, Proc. of the 10th NASA Formal Methods Symposium (NFM 2018), vol.10811, pp.37-53, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01720401
, , 2018.
Proving Consistency and Completeness of Model Classes Using Theory Interpretation, Proc. of the 13th International Conference on Fundamental Approaches to Software Engineering (FASE 2010), vol.6013, pp.218-232, 2010. ,
Auto-Active Proof of Red-Black Trees in SPARK, NASA Formal Methods -9th International Symposium, pp.68-83, 2017. ,
Contiki -A Lightweight and Flexible Operating System for Tiny Networked Sensors, 2004. ,
,
, Why3 -Where Programs Meet Provers, ESOP 2013
Specifying linked data structures in JML for combining formal verification and testing, Science of Computer Programming, pp.19-40, 2015. ,
A Certified Multiprover Verification Condition Generator, Verified Software: Theories, Tools, Experiments (VSTTE), vol.7152, pp.2-17, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00639977
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, Nasa Formal Methods (NFM) (LNCS), pp.41-55, 2011. ,
, Julien Signoles, and Boris Yakobowski. 2015. Frama-C: A software analysis perspective. Formal Asp. Comput, vol.27, pp.573-609, 2015.
A Lesson on Runtime Assertion Checking with Frama-C, Runtime Verification (RV), vol.8174, pp.386-399, 2013. ,
URL : https://hal.archives-ouvertes.fr/cea-01834991
Usable Auto-Active Verification, 2010. ,
Ghosts for Lists: from Axiomatic to Executable Specifications, Proc. of the 12th International Conference on Tests and Proofs (TAP 2018) (LNCS), vol.10889, pp.177-184, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01811922
A Memory Allocation Module of Contiki Formally Verified with Frama-C. A Case Study, CRiSIS 2016, vol.10158, 2016. ,
A Verified Messaging System, Proc. ACM Program. Lang. 1, OOPSLA, Article, vol.87, 2017. ,
Towards Formal Verification of Contiki OS: Analysis of the AES-CCM* Modules with Frama-C, RED-IoT, 2018. ,
Software verification with VeriFast: Industrial case studies, Science of Computer Programming, vol.82, pp.77-97, 2014. ,
Specifying Reusable Components, Proc. of the 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE 2010), vol.6217, pp.127-141, 2010. ,
Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS), pp.55-74, 2002. ,
, The Coq Development Team
, The Coq Proof Assistant
Featherweight VeriFast, Logical Methods in Computer Science, vol.11, p.19, 2015. ,
Verified Correctness and Security of mbedTLS HMAC-DRBG, ACM SIGSAC Conference on Computer and Communications Security (CCS), 2007. ,