In short ...

I am Full Professor at the University Paris-Sud (Orsay) and member of the Laboratoire de Recherche Informatique (LRI) which is a research institution belonging to the CNRS. I am co-director(co-responsable) of the Team VALS (Verification of Algorithms, Languages and Systems), a merger of the former Toccata and ForTesSE teams (official site of the latter, group wiki).

My research interests are focussed on Software Verification Environments. This covers top-down refinement methods (like HOL-Z or HOL-OCL), bottum-up code verification methods (like IMP++ based on HOL-OCL or HOL-Boogie) or specification-based testing methods (like HOL-TestGen). I consider myself as a "Formal Methodist" in Software Engineering.

My research activities comprise the semantic representation of programming and specification languages by means of logical embeddings in Isabelle, the development of specialized automated proof procedures, tool-support for refinement techniques and for compilation to code, and automated techniques to generate tests from specifications and programs. My interest in tool development also covers tool-integration aspects and the design of appropriate user-interfaces.

I have a longstanding interest in the application of verification and testing techniques in the field of computer security, and a more recent one in applications in operating systems and computer architecture.