burkhart.wolff

My research interests are in the field of model-based software development as well as quality assurence by validation and verification. In particular, my research is focussed on the integration of formal foundations and proof techniques into the model-driven software engineering and model-based testing techniques. This comprises work on the semantic foundation of specification and programming languages, the development of calculi for refinement and test-generation as well as the construction of correct tools in order to support these activities during design, verification, systematic test and certification.

Particular application fields of these techniques have been models of security mechanisms and (more recently) operating systems.

A a mission, I believe in Unity within Computer Science - we should strive for a few principles and tools to solve the problems ahead instead diving into too many local techniques.

• The Isabelle/DOF project (GIT, Founding Paper: Isabelle/DOF: Design and Implementation., Journal Paper
• The Isabelle/C project (GIT,The Isabelle/C bundle, Paper), with semantic backends to CLean and AutoCorres.
• The HOL-CSP project ( AFP HOL-CSP core, AFP HOL-CSPM, AFP CSP Refinement Toolkit, AFP HOL-CSP Operational Semantics Derived, AFP Restriction Spaces, AFP Restriction Spaces II , AFP Restriction Spaces III, AFP Restriction Spaces IV)
• The subsequent OVH and SVR projects affiliated at the Institut de Recherche en Technologie SystemX is concerned with collective autonomous transport systems (shuttle busses and robot-taxis level 5). Our contribution is to provide formal models allowing simulation, test and proof in order to establish security in all circumstances.

• The project PST Performances des Systemes de Transport at SystemX (June. 2016 - June. 2019). The new generations of transport system equipment must be able to integrate monitoring, communication and optimization functions (cyber security, data collection, energy saving etc.) while at the same time ensuring safe, high performance operation of the basic functions of control/command. In a sub-project called T4, an integrated formal development has been undertaken together with the development of a specific "continuous verification/continuous-build" tool-chain based on Isabelle/HOL. Managing an integrated document, it is designed to assure the global coherence from models, designs, code, tests and thorough documentation of the process targeting formal certification following CENELEC.
• The EU-Project EUROMILS (Oct. 2012 - Sept. 2015 ). The projects cornerstone is MILS (Multiple Independent Levels of Security), a high-assurance security operating system that supports the coexistence of untrusted and trusted components, based on verifiable separation mechanisms and controlled information flow. For the first time in Europe, EURO-MILS does a complete Common Criteria security evaluation of a MILS system to its highest levels of assurance, including formal verification engineering. Hardware dependencies are addressed from the beginning by prototype development on two hardware platforms in automotive and avionics.
• The ANR-project Paral-ITP (Nov. 2011 - Apr. 2015) with the Project Partners are INRIA Roquencourt (Hugo Herbelin), INRIA Saclay (Bruno Barras) and U-PSud/LRI (B.Wolff, Project Leader).
  The proposed project intends to overcome the sequential model both for Coq and Isabelle, to make the resources of multi-core hardware available for even larger proof developments. Beyond traditional processing of proof scripts as sequence of proof commands, and batch-loading of theory modules, there is a large space of possibilities and challenges for pervasive parallelism. This affects many layers of each prover system: basic computational structures, inference kernel, tactical programming, proof command language, and interactive front-ends.
• The HOL-TestGen-XT project (2009-2012) was accepted as part of the "Chair d'excellence" program of the University Paris-Sud. The ultimate goal of this research proposal was to extend the realm of feasible state-spaces for HOL-TestGen system (see below) by several orders of magnitude - thus offering even more potential for industrial applications in realistic model-based test-scenarios.
  
• I was initiator of the project MBT-SEC, funded by British-Telecom (2007-2010). The goal was to use Security policies as model-based specifications for system behaviour and to derive test-cases for them.
• I was invited researcher in the FSE group (headed by Dr. Wolfram Schulte) at Microsoft Research, Redmond, USA. I investigated ways of an extension of the existing Boogie-Codeverification Tool for the programming language C with interactive proof techniques supported by Isabelle/HOL.