Frama-C: A software analysis perspective, Formal Aspects of Computing, pp.573-609, 2015. ,
URL : https://hal.archives-ouvertes.fr/cea-01808981
ACSL: ANSI/ISO C Specification Language ,
MetAcsl: Specification and Verification of High-Level Properties, Tools and Algorithms for the Construction and Analysis of Systems, pp.358-364, 2019. ,
URL : https://hal.archives-ouvertes.fr/cea-02019790
, WP plugin manual
E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper), International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, pp.164-173, 2017. ,
How testing helps to diagnose proof failures, Formal Aspects of Computing, pp.629-657, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01948799
JML: A Notation for Detailed Design, Behavioral Specifications of Businesses and Systems, pp.175-188, 1999. ,
Specifying and Checking Method Call Sequences in JML, International Conference on Software Engineering Research and Practice, pp.511-516, 2005. ,
Extending JML Specifications with Temporal Logic, International Conference on Algebraic Methodology and Software Technology. AMAST, pp.334-348, 2002. ,
Vérification de propriétés LTL sur des programmes C par génération d'annotations, 2011. ,
CaFE: a model-checker collaboratif, Approches Formelles dans l'Assistance au Developpement Logiciel, 2017. ,
Static and Dynamic Verification of Relational Properties on Self-composed C Code, International Conference on Tests and Proofs, 2018. ,
URL : https://hal.archives-ouvertes.fr/cea-01835470
Enforcing High-Level Security Properties for Applets, International Conference on Smart Card Research and Advanced Applications, pp.1-16, 2004. ,
URL : https://hal.archives-ouvertes.fr/inria-00071523
Aspect-Oriented Programming, European Conference on Object-Oriented Programming, pp.220-242, 1997. ,