Formally verified differential dynamic logic

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

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

24 Citations (Scopus)
78 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017
EditorsYves Bertot, Viktor Vafeiadis
PublisherAssociation for Computing Machinery (ACM)
Pages208-221
Number of pages14
ISBN (Print)978-1-4503-4705-1
DOIs
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
Country/TerritoryFrance
CityParis
Period16/01/1717/01/17

Fingerprint

Dive into the research topics of 'Formally verified differential dynamic logic'. Together they form a unique fingerprint.

Cite this