Formally verified differential dynamic logic
Open Access
- 16 January 2017
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 208-221
- https://doi.org/10.1145/3018610.3018616
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.Keywords
Funding Information
- Defense Advanced Research Projects Agency (FA8750-12-2-0291)
- National Science Foundation (CNS-1054246)
- Fonds National de la Recherche Luxembourg (FNR/P14/8149128)
This publication has 27 references indexed in Scilit:
- Coquelicot: A User-Friendly Library of Real Analysis for CoqMathematics in Computer Science, 2014
- Towards a Formally Verified Proof AssistantLecture Notes in Computer Science, 2014
- Steps towards Verified Implementations of HOL LightLecture Notes in Computer Science, 2013
- SpaceEx: Scalable Verification of Hybrid SystemsLecture Notes in Computer Science, 2011
- Real World VerificationLecture Notes in Computer Science, 2009
- Differential Dynamic Logic for Hybrid SystemsJournal of Automated Reasoning, 2008
- Innovations in computational type theory using NuprlJournal of Applied Logic, 2006
- Towards Self-verification of HOL LightLecture Notes in Computer Science, 2006
- Nominal Logic: A First Order Theory of Names and BindingLecture Notes in Computer Science, 2001
- Hybrid systems in TLA+Lecture Notes in Computer Science, 1993