Why Hi-Lite Ada?, Boogie, pp.27-39, 2011. ,
Boogie: A Modular Reusable Verifier for Object-Oriented Programs, In: FMCO. LNCS, vol.4111, 2005. ,
DOI : 10.1007/11804192_17
Why3: Shepherd your herd of provers, In: Boogie, pp.53-64, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00790310
Expressing Polymorphic Types in a Many-Sorted Language, In: FroCoS. LNCS, vol.40, issue.1, pp.87-102, 2011. ,
DOI : 10.1007/978-3-540-78800-3_24
URL : https://hal.archives-ouvertes.fr/inria-00591414
Fast Pattern Matching in Strings, SIAM Journal on Computing, vol.6, issue.2, pp.323-350, 1977. ,
DOI : 10.1137/0206024
VACID-0: Verification of ample correctness of invariants of data-structures, edition 0, 2010. ,