1. Alfred V. Aho, Monica S. Lam, Ravi Sethi & Jeffrey D. Ullman (2006): Compilers: Principles, Techniques, and Tools (2Nd Edition). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.
  2. Martin Clochard & Léon Gondelman (2015): Double WP : Vers une preuve automatique d'un compilateur. In: Journées Francophones des Langages Applicatifs, Val d'Ajol, France, pp. 1–18. Available at
  3. Jean-Christophe Filliâtre & Martin Clochard (2013): A tiny register allocator for tree expressions. Online; accessed May 15th 2018.
  4. Sabine Glesner, Simone Forster & Matthias Jäger (2005): A Program Result Checker for the Lexical Analysis of the GNU C Compiler. Electr. Notes Theor. Comput. Sci. 132(1), pp. 19–35, doi:10.1016/j.entcs.2005.01.029.
  5. Léon Gondelman & Martin Clochard (2013): Double WP. Online; accessed May 15th 2018.
  6. Jason Hickey, Anil Madhavapeddy & Yaron Minsky (2014): Real World OCaml. "O'Reilly Media, Inc.". Available at
  7. Inria (2013): Why3 - Home. Online; accessed May 15th 2018.
  8. Xavier Leroy (2009): Formal verification of a realistic compiler. Communications of the ACM 52(7), pp. 107–115, doi:10.1145/1538788.1538814. Available at
  9. Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin & Steve Zdancewic (2012): Formalizing the LLVM intermediate representation for verified program transformations.. In: John Field & Michael Hicks: POPL. ACM, pp. 427–440, doi:10.1145/2103656.2103709. Available at

Comments and questions to:
For website issues: