The B-Book, assigning programs to meaning, 1996. ,
Deductive Software Verication -The KeY Book -From Theory to Practice, Lecture Notes in Computer Science, vol.10001, 2016. ,
Boogie: A Modular Reusable Verier for Object-Oriented Programs, Formal Methods for Components and Objects: 4th International Symposium, vol.4111, p.364387, 2005. ,
ACSL: ANSI/ISO C Specication Language, version 1, vol.4, 2009. ,
An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer (STTT), vol.7, issue.3, p.212232, 2005. ,
SPARKan annotated Ada subset for safety-critical programming, Proceedings of the conference on TRI-ADA'90, TRI-Ada'90, p.392402, 1990. ,
Characteristic formulae for the verication of imperative programs, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (ICFP), p.418430, 2011. ,
GOSPEL providing OCaml with a formal specication language, FM 2019 23rd International Symposium on Formal Methods, 2019. ,
Mário Pereira, and François Pottier. VOCAL A Veried OCaml Library. ML Family Workshop, 2017. ,
Verifying the correctness and amortized complexity of a union-nd implementation in separation logic with time credits, Journal of Automated Reasoning, vol.62, issue.3, p.331365, 2019. ,
How to avoid proving the absence of integer overows, 7th Working Conference on Veried Software: Theories, Tools and Experiments (VSTTE), vol.9593, p.94109, 2015. ,
VCC: Contract-based modular verication of concurrent C, 31st International Conference on Software Engineering, p.429430, 2009. ,
Why3 where programs meet provers, KeY Symposium 2017, 2017. ,
A pragmatic type system for deductive verication, 2016. ,
The spirit of ghost code, Formal Methods in System Design, vol.48, issue.3, p.152174, 2016. ,
Why3 where programs meet provers, Proceedings of the 22nd European Symposium on Programming, vol.7792, p.125128, 2013. ,
VeriFast: A powerful, sound, predictable, fast verier for C and Java, NASA Formal Methods, vol.6617, p.4155, 2011. ,
A formally-veried C static analyzer, 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p.247259, 2015. ,
Frama-c: A software analysis perspective, Formal Aspects of Computing, vol.27, issue.3, p.573609, 2015. ,
URL : https://hal.archives-ouvertes.fr/cea-01808981
Dafny: An automatic program verier for functional correctness, LPAR-16, vol.6355, p.348370, 2010. ,
A formally veried compiler back-end, Journal of Automated Reasoning, vol.43, issue.4, p.363446, 2009. ,
PVS: A prototype verication system, 11th International Conference on Automated Deduction, p.748752, 1992. ,
Tools and Techniques for the Verication of Modular Stateful Code, 2018. ,
A fully veried container library, Formal Asp. Comput, vol.30, issue.5, p.495523, 2018. ,
Verifying a hash table and its iterators in higher-order separation logic, Proceedings of the 6th ACM SIGPLAN Conference on Certied Programs and Proofs, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01417102
Coq coq correct! verication of type checking and erasure for coq, in coq, Proc. ACM Program. Lang, vol.4, 2019. ,
Dependent types and multi-monadic eects in F*, 43rd ACM Symposium on Principles of Programming Languages (POPL), p.256270, 2016. ,
, The Coq Development Team. The Coq Proof Assistant Reference Manual Version V8, vol.9, 2019.
Autoproof: Auto-active functional verication of object-oriented programs, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2015. ,