Formally verified differential dynamic logic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

  • Brandon Bohrer
  • Vincent Rahli
  • Ivana Vukotic
  • Marcus Völp
  • André Platzer

Colleges, School and Institutes

Abstract

We formalize the soundness theorem for differential dynamic logic, a logic for verifying hybrid systems. To increase confidence in the formalization, we present two versions: one in Isabelle/HOL and one in Coq. We extend the metatheory to include features used in practice, such as systems of differential equations and functions of multiple arguments. We demonstrate the viability of constructing a verified kernel for the hybrid systems theorem prover KeYmaera X by embedding proof checkers for differential dynamic logic in Coq and Isabelle. We discuss how different provers and libraries influence the design of the formalization.

Details

Original languageEnglish
Title of host publicationProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017
EditorsYves Bertot, Viktor Vafeiadis
Publication statusPublished - 16 Jan 2017
Event6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017 - Paris, France
Duration: 16 Jan 201717 Jan 2017

Conference

Conference6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017
CountryFrance
CityParis
Period16/01/1717/01/17