Abstract

While Formal Testing and Theorem-Proving are still perceived as antagonisms by many, there is a growing research field using the combination of both to increase the applicability of Formal Methods in industry, in particular in the area of Safety-and Security critical systems requiring formal certifications.

In this talk, Burkhart Wolff will present research (partially funded by Digiteo) around the HOL-TestGen System, which strives for a synthesis of interactive and automated theorem proving as well of different formal testing techniques.

Burkhart Wolff will present results which are of mutual interest for both research areas as well as an outlook for future
directions.

Bio
Burkhart Wolff's research interests are in the field of modeling and model-based software development as well as quality assurence by validation and verification. In particular, his research has been focussed on the integration of formal foundations and proof techniques into the model-driven engineering approach (MDE) and model-based testing techniques into software development.

This captures the foundation of specification and programming languages and the construction of correct tools - based on interactive and automated theorem proving techniques - in order to support these activities during design, verification and systematic test.

Particular application fields of these techniques have been models of operating systems and their security mechanisms.