Véronique Cortier @ LORIA CNRS, INRIA & Université de Lorraine
Véronique Cortier is Senior Researcher of the CNRS working in the LORIA laboratory. Her research interests include electronic voting protocols (see the system Belenios), verification of security protocols, link between symbolic and cryptographic models for protocols and automatic deduction, tree automata.
Marieke Huisman @ University of Twente
Marieke Huisman is Professor in Software Reliability, leading the FMT (Formal Methods and Tools) Group at the University of Twente. Her research topics includes program verification, reliability of concurrent, parallel and distributed applications
software specification and formal methods.
André Platzer @ Karlsruhe Institute of Technology || Carnegie Mellon University
André Platzer is the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems at Karlsruhe Institute of Technology and a Professor of Computer Science at Carnegie Mellon University. He develops logics for dynamical systems to characterize the logical foundations of cyber-physical systems and to answer the question how we can trust a computer to control physical processes. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. Prof. Platzer pursues this challenge with the principled design of programming languages with logics that can provide proofs as correctness guarantees.
Burkhart Wolff@ University Paris Saclay || Laboratoire des Méthodes Formelles (LMF)
Burkhart Wolff’s 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. He is called a “Formal Methodist” in Software Engineering. His research activities comprise the semantic representation of programming and specification languages by means of logical embeddings, and the development of specialized automated proof procedures. His activities in tool development also cover tool-integration aspects and the design of appropriate user-interfaces. He also works on ontological methods to assure the traceability in integrated sources of system developments.
