Nearly all binary searches and mergesorts are broken, 2006. ,
The Astrée static analyzer http ,
SMT-based bounded model checking for embedded ANSI-C software, Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering. ASE '09, pp.137-148, 2009. ,
Types, bytes, and separation logic, Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07), pp.97-108, 2007. ,
Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013. ,
DOI : 10.1007/978-3-642-37036-6_8
Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Proc. of the Koninklijke Nederlands Akademie, pp.380-392, 1972. ,
Group Characters and Algebra. Philosophical transactions of the Royal Society of London: Mathematical and physical sciences, 1934. ,
DOI : 10.1098/rsta.1934.0015
Why3: Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, pp.53-64, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00790310
One Logic to Use Them All, 24th International Conference on Automated Deduction, pp.1-20, 2013. ,
DOI : 10.1007/978-3-642-38574-2_1
The spirit of ghost code, 26th International Conference on Computer Aided Verification, pp.1-16, 2014. ,
An algorithm for the organization of information, Soviet Mathematics?Doklady, vol.3, issue.5, pp.1259-1263, 1962. ,