Proof Assistants and Related Tools - The PART & PART 2 Projects, Workshops 9+13 November 2017

Program for Thursday 9 November 2017 - DTU room 101/S16

• 13:30-14:00 Jørgen Villadsen (DTU Compute, joint work with Anders Schlichtkrull and Andreas Halkjær From): A Certified Simple Prover for First-Order Logic
• 14:00-15:00 Freek Wiedijk (Radboud University, Nijmegen, The Netherlands): Trust
• 15:00-15:30 Anders Schlichtkrull (DTU Compute): IsaFoL - Isabelle Formalization of Logic - A Brief Overview

• 13:00-14:00 Stefan Berghofer (secunet Security Networks AG, Dresden, Germany): Development of Security-Critical Software with SPARK/Ada at secunet
• 14:30-15:30 Christian Sternagel (University of Innsbruck, Austria): IsaFoR/CeTA - An Isabelle/HOL Formalization of Rewriting for Certified Tool Assertions

Abstract for the talk by Freek Wiedijk: I will discuss how trustworthy a formal proof (checked with an interactive theorem prover like Coq, Isabelle or one of the HOLs) can be, both in theory and in practice. I will illustrate this by explaining the current state of the art and by discussing possible new technologies.

Abstract for the talk by Stefan Berghofer: In this talk, we describe how the SPARK/Ada language and toolset is used for the development of component-based high-security systems at secunet Security Networks AG. To make the complexity of assessing the security of these systems manageable, the components are running on top of a separation kernel, which ensures that they can only communicate with each other via designated channels. We give an overview of our methodology for verifying trusted components using a combination of the SPARK tools and the interactive proof assistant Isabelle, which is used for solving proof obligations that are beyond reach of automatic provers. We illustrate the methodology using selected correctness properties of a cryptographic library.

Abstract for the talk by Christian Sternagel: I will give a general overview of the ongoing IsaFoR/CeTA project and its two main components: (1) the IsaFoR proof library for Isabelle/HOL, focusing on term rewriting related properties (like termination, confluence, and completion) and (2) the accompanying, formally verified certifier CeTA, obtained by code generation.

All are welcome. Registration is not necessary. More information is available here: http://part.compute.dtu.dk/

Organizers: Michael Reichhardt Hansen, Anne Elisabeth Haxthausen, Sebastian Alexander Mödersheim and Jørgen Villadsen (DTU Compute)

Supported by DTU Compute's Strategic Foundation