burkhart.wolff

I am Full Professor at the University Paris-Saclay and member of the Laboratoire des Methodes Formelles (LMF), a merger of the teams VALS (Verification of Algorithms, Languages and Systems), and the LSV of the former ENS Cachan.

My research interests are focussed on formal software engineering comprising specification and verification.

The latter covers top-down refinement methods, bottum-up code verification as well as formal testing methods. Implementations, theories and tools are developed for the Isabelle/HOL-platform. I have been called a "Formal Methodist" in Software Engineering.

My research activities comprise the semantic representation of programming and specification languages by means of logical embeddings, and the development of specialized automated proof procedures. My activities in tool development also cover tool-integration aspects and the design of appropriate user-interfaces. I also work on ontological methods to assure the traceability in integrated sources of system developments.

I have a longstanding interest in the application of modeling and verification techniques in the field of computer security, operating systems and computer architecture.