ACSL: ANSI/ISO C Specification Language, version 1, vol.4, 2009. ,
Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo automated theorem prover, 2008. ,
SPARK-an annotated Ada subset for safety-critical programming, Proceedings of the conference on TRI-ADA'90, TRI-Ada'90, pp.392-402, 1990. ,
A verified implementation of the bounded list container, Tools and Algorithms for the Construction and Analysis of Systems, pp.172-189, 2018. ,
Characteristic Formulae for Mechanized Program Verification, 2010. ,
Characteristic formulae for the verification of imperative programs, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (ICFP), pp.418-430, 2011. ,
Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, Journal of Automated Reasoning, 2017. ,
Temporary read-only permissions for separation logic, Proceedings of the European Symposium on Programming, 2017. ,
The ASTRÉE analyzer, ESOP, number 3444 in Lecture Notes in Computer Science, pp.21-30, 2005. ,
, , 2019.
Verifying openjdk's sort method for generic collections, Journal of Automated Reasoning, 2017. ,
One logic to use them all, 24th International Conference on Automated Deduction, vol.7898, pp.1-20, 2013. ,
Why3 -where programs meet provers, Proceedings of the 22nd European Symposium on Programming, vol.7792, pp.125-128, 2013. ,
A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification, ESOP 2018 -27th European Symposium on Programming, vol.10801, 2018. ,
Behavioral interface specification languages, ACM Comput. Surv, vol.44, issue.3, 2012. ,
An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969. ,
VeriFast: A powerful, sound, predictable, fast verifier for C and Java, NASA Formal Methods, vol.6617, pp.41-55, 2011. ,
Tutorial for the 2nd COST Action IC0701 Training School, Limerick 6/11, 2011. ,
The dynamic frames theory, Formal Aspects of Computing, vol.23, issue.3, pp.267-288, 2011. ,
Frama-c: A software analysis perspective, Formal Aspects of Computing, vol.27, issue.3, pp.573-609, 2015. ,
URL : https://hal.archives-ouvertes.fr/cea-01808981
seL4: Formal verification of an OS kernel, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010. ,
Static versus dynamic verification in Why3, Frama-C and SPARK, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), vol.9952, pp.461-478, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01344110
Preliminary design of JML: A behavioral interface specification language for Java, 2000. ,
Dafny: An automatic program verifier for functional correctness, LPAR-16, vol.6355, pp.348-370, 2010. ,
A basis for verifying multi-threaded programs, Programming Languages and Systems, pp.378-393, 2009. ,
A formally verified compiler back-end, Journal of Automated Reasoning, vol.43, issue.4, pp.363-446, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00360768
Viper: A verification infrastructure for permission-based reasoning, Verification, Model Checking, and Abstract Interpretation (VMCAI), vol.9583, pp.41-62, 2016. ,
Time credits and time receipts in Iris, European Symposium on Programming, vol.11423, pp.1-27, 2019. ,
The relationship between separation logic and implicit dynamic frames, Logical Methods in Computer Science, vol.8, issue.3, 2012. ,
Tools and Techniques for the Verification of Modular Stateful Code, 2018. ,
URL : https://hal.archives-ouvertes.fr/tel-01980343
A fully verified container library, Formal Asp. Comput, vol.30, issue.5, pp.495-523, 2018. ,
Separation logic: a logic for shared mutable data structures, 17th Annual IEEE Symposium on Logic in Computer Science, 2002. ,
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 (RV-CuBES'17), 2017. ,
Implicit dynamic frames: Combining dynamic frames and separation logic, ECOOP 2009 -Object-Oriented Programming, pp.148-172, 2009. ,
, The Coq Development Team. The Coq Proof Assistant Reference Manual -Version V8, vol.9, 2019.