Formally verified differential dynamic logic

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

doi:10.1145/3018610.3018616

Formally verified differential dynamic logic

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

24 Citations (Scopus)

134 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 language	English
Title of host publication	Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017
Editors	Yves Bertot, Viktor Vafeiadis
Publisher	Association for Computing Machinery (ACM)
Pages	208-221
Number of pages	14
ISBN (Print)	978-1-4503-4705-1
DOIs	https://doi.org/10.1145/3018610.3018616
Publication status	Published - 16 Jan 2017
Event	6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017 - Paris, France Duration: 16 Jan 2017 → 17 Jan 2017

Conference

Conference	6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017
Country/Territory	France
City	Paris
Period	16/01/17 → 17/01/17

Access to Document

10.1145/3018610.3018616Licence: None: All rights reserved

Brandon_Bohrer_et_al_Formally_verified_differential_dynamic_logic_CPP_2017_2017
Checked for eligibility: 22/07/2019 © ACM 2017. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in CPP 2017 Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, http://dx.doi.org/10.1145/3018610.3018616.
Accepted author manuscript, 356 KBLicence: Other (please specify with Rights Statement)

https://doi.org/10.1145/3018610.3018616Licence: None: All rights reserved

Cite this

@inproceedings{3bdc8e075ad048fa965c3713188cba42,

title = "Formally verified differential dynamic logic",

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. ",

author = "Brandon Bohrer and Vincent Rahli and Ivana Vukotic and Marcus V{\"o}lp and Andr{\'e} Platzer",

year = "2017",

month = jan,

day = "16",

doi = "10.1145/3018610.3018616",

language = "English",

isbn = "978-1-4503-4705-1",

pages = "208--221",

editor = "Yves Bertot and Viktor Vafeiadis",

booktitle = "Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

note = "6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017 ; Conference date: 16-01-2017 Through 17-01-2017",

}

Bohrer, B, Rahli, V, Vukotic, I, Völp, M & Platzer, A 2017, Formally verified differential dynamic logic. in Y Bertot & V Vafeiadis (eds), Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017. Association for Computing Machinery (ACM), pp. 208-221, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, 16/01/17. https://doi.org/10.1145/3018610.3018616

Formally verified differential dynamic logic. / Bohrer, Brandon; Rahli, Vincent; Vukotic, Ivana et al.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017. ed. / Yves Bertot; Viktor Vafeiadis. Association for Computing Machinery (ACM), 2017. p. 208-221.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Formally verified differential dynamic logic

AU - Bohrer, Brandon

AU - Rahli, Vincent

AU - Vukotic, Ivana

AU - Völp, Marcus

AU - Platzer, André

PY - 2017/1/16

Y1 - 2017/1/16

N2 - 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.

AB - 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.

U2 - 10.1145/3018610.3018616

DO - 10.1145/3018610.3018616

M3 - Conference contribution

SN - 978-1-4503-4705-1

SP - 208

EP - 221

BT - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017

A2 - Bertot, Yves

A2 - Vafeiadis, Viktor

PB - Association for Computing Machinery (ACM)

T2 - 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017

Y2 - 16 January 2017 through 17 January 2017

ER -

Formally verified differential dynamic logic

Abstract

Conference

Access to Document

Fingerprint

Cite this