The question of formally proving that programs comply with properties describing their specification is a notoriously complex and polymorphic problem. Several development environments attempt to bring answers. In this talk, we will present one of them, FoCaLiZe, allowing, inside a same programming language, to deal with algorithms, properties and proofs, while trying to keep simple enough and close to usual programming languages. The presentation will address the features of the language and shortly its compilation. FoCaLiZe generates OCaml, Coq and Dedukti codes to obtain both an executable (or a library) and a complete formal model of the program, its properties and their proofs. This model is sent to a formal checker to double-check the validity of the development. FoCaLiZe applies a common compilation trunk and code generation model to ensure a good traceability between the produced codes.
François Pessaux has been Professor Associate at ENSTA ParisTech for 7 years. He did his PhD thesis in the Cristal project at INRIA from 1997 to 1999 on the analysis of uncaught exception in OCaml. He then spent one and half year in a post-doctoral position at Lucent / Hoboken University in the USA, before coming back in France where he led 6 year ago the R&D department at SURLOG, company specialized in safety analyses. He came back in the academic world on a 2 years contract at LIP6 where he developed FoCaLiZe on the basis of Focal. He then worked one year in KALRAY to develop, among other things, a prototype of scheduler for a massively parallel architecture and an Eclipse plugin for the programming language supporting this architecture. Finally, during one year he re-designed the typechecker of the OPA programming language at MLstate before joining the ENSTA ParisTech.
Host: Manuel Maarek