1 July 2019 - Brandon Bohrer (Carnegie Mellon University) Abstract In the world of theorem provers, we always try to base our tools on a logic with solid formal foundations.However, in the process of doing serious proofs in our tool, we often find that practical work demands features which were not addressed in the foundations, resulting in a larger and more complex prover, or otherwise less trustworthy prover core. Examples include context management in NuPrl, termination-checking in Coq, and partial or discontinuous functions in KeYmaera X, the latter being the focus of this talk. When tools outgrow their foundations, it is essential to bring foundations back up speed with implementation to ensure trustworthiness. In this talk, we bring differential dynamic logic (dL), a logic for verifying hybrid-systems models of safety-critical cyber-physical systems, up to speed with its implementation in the prover KeYmaera X. We do so by introducing dLι, which extends dL for hybrid systems with definite descriptions and tuples. Definite descriptions enable partial, nondifferentiable, and discontinuous terms, which have many examples in applications, such as divisions, nth roots, and absolute values. Tuples enable systems of multiple differential equations, arising in almost every application. Together, definite description and tuples combine to support long-desired features such as vector arithmetic. We discuss and overcome the unique challenges posed by extending dL with these features. Unlike in dL, definite descriptions enable non-locally-Lipschitz terms, so our differential equation (ODE) axioms now make their continuity requirements explicit. Tuples are trivial when considered in isolation, but in the context of hybrid systems they demand that differentials are treated in full generality. The addition of definite descriptions also makes dLι a free logic; we investigate the interaction of free logic and the ODEs of dL, showing that this combination is sound, and characterize its expressivity. We give an example system that can be defined and verified using these extensions. Biography Brandon Bohrer is a rising 5th-year PhD Student at Carnegie Mellon University, where he also received his undergraduate degree. He works in Andre Platzer's Logical Systems Lab dedicated to theorem proving for cyber-physical systems. His research focuses generally on connecting rigorous foundations for hybrid systems proving to practical applications of those verified systems. He publishes in conferences such as LICS, CADE, PLDI, ITP, and CPP. He is funded by the National Defense Science and Engineering Graduate (NDSEG) Fellowship and has also received the Alan Perlis Award for his graduate teaching at CMU. Jul 01 2019 11.00 - 12.00 1 July 2019 - Brandon Bohrer (Carnegie Mellon University) Definite Descriptions in Differential Dynamic Logic: Extensible Foundations for Practical Hybrid Systems Proving IF 4.31/33
1 July 2019 - Brandon Bohrer (Carnegie Mellon University) Abstract In the world of theorem provers, we always try to base our tools on a logic with solid formal foundations.However, in the process of doing serious proofs in our tool, we often find that practical work demands features which were not addressed in the foundations, resulting in a larger and more complex prover, or otherwise less trustworthy prover core. Examples include context management in NuPrl, termination-checking in Coq, and partial or discontinuous functions in KeYmaera X, the latter being the focus of this talk. When tools outgrow their foundations, it is essential to bring foundations back up speed with implementation to ensure trustworthiness. In this talk, we bring differential dynamic logic (dL), a logic for verifying hybrid-systems models of safety-critical cyber-physical systems, up to speed with its implementation in the prover KeYmaera X. We do so by introducing dLι, which extends dL for hybrid systems with definite descriptions and tuples. Definite descriptions enable partial, nondifferentiable, and discontinuous terms, which have many examples in applications, such as divisions, nth roots, and absolute values. Tuples enable systems of multiple differential equations, arising in almost every application. Together, definite description and tuples combine to support long-desired features such as vector arithmetic. We discuss and overcome the unique challenges posed by extending dL with these features. Unlike in dL, definite descriptions enable non-locally-Lipschitz terms, so our differential equation (ODE) axioms now make their continuity requirements explicit. Tuples are trivial when considered in isolation, but in the context of hybrid systems they demand that differentials are treated in full generality. The addition of definite descriptions also makes dLι a free logic; we investigate the interaction of free logic and the ODEs of dL, showing that this combination is sound, and characterize its expressivity. We give an example system that can be defined and verified using these extensions. Biography Brandon Bohrer is a rising 5th-year PhD Student at Carnegie Mellon University, where he also received his undergraduate degree. He works in Andre Platzer's Logical Systems Lab dedicated to theorem proving for cyber-physical systems. His research focuses generally on connecting rigorous foundations for hybrid systems proving to practical applications of those verified systems. He publishes in conferences such as LICS, CADE, PLDI, ITP, and CPP. He is funded by the National Defense Science and Engineering Graduate (NDSEG) Fellowship and has also received the Alan Perlis Award for his graduate teaching at CMU. Jul 01 2019 11.00 - 12.00 1 July 2019 - Brandon Bohrer (Carnegie Mellon University) Definite Descriptions in Differential Dynamic Logic: Extensible Foundations for Practical Hybrid Systems Proving IF 4.31/33
Jul 01 2019 11.00 - 12.00 1 July 2019 - Brandon Bohrer (Carnegie Mellon University) Definite Descriptions in Differential Dynamic Logic: Extensible Foundations for Practical Hybrid Systems Proving
