KeYmaera User Tutorial: How to Prove Complex Properties of Hybrid Systems with KeYmaera

Table of Contents
  1. KeYmaera User Tutorial
  2. Abstract
  3. Selected Publications
Download or
WebstartKeYmaera
Logical Analysis of Hybrid Systems

KeYmaera User Tutorial

 

This is a preliminary page with a more detailed user description on how to use KeYmaera to model and prove properties. More details will be coming up at some point.

Abstract

This paper is a tutorial on how to model and prove complex properties of complex hybrid systems in KeYmaera [4], an automatic and interactive formal verification tool for hybrid systems implementing differential dynamic logic [7,6]. Hybrid systems can model highly nontrivial controllers of physical plants, whose behaviors are often safety critical such as trains, cars, airplanes, or medical devices. Formal methods can help design systems that work correctly. This paper illustrates how KeYmaera can be used to systematically model, validate, and verify hybrid systems. We develop tutorial examples that illustrate challenges arising in many real-world systems. In the context of this tutorial, we identify the impact that modeling decisions have on the suitability of the model for verification purposes. We show how the interactive features of KeYmaera can help users understand their system designs better and prove complex properties for which the automatic prover of KeYmaera still takes an impractical amount of time. We hope this paper is a helpful resource for designers of embedded and cyber-physical systems and that it illustrates how to master common practical challenges in hybrid systems verification.

Keywords: formal verification of hybrid systems, differential dynamic logic, automated theorem proving, introduction to hybrid system modeling and verification

Selected Publications

The canonical references on the KeYmaera approach are [6] and [5]. The most comprehensive description of the KeYmaera appraoch can be found in the book [2]. Also see the publication reading guide.
  1. André Platzer.
    Logics of dynamical systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012. © IEEE
    Invited paper.
    [bib | pdf | doi | slides | abstract]

  2. André Platzer.
    Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
    Springer, 2010. 426 p. ISBN 978-3-642-14508-7.
    [bib | book | eBook | doi | web]

  3. André Platzer.
    Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems.
    PhD Thesis, Department of Computing Science, University of Oldenburg, 2008.
    ACM Doctoral Dissertation Honorable Mention Award in 2009.
    Extended version appeared as book Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, 2010.
    [bib | pdf | eprint | book | doi | web | abstract | slides]

  4. André Platzer and Jan-David Quesel.
    KeYmaera: A hybrid theorem prover for hybrid systems.
    In Alessandro Armando, Peter Baumgartner and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pages 171-178. Springer, 2008. © Springer-Verlag
    [bib | pdf | doi | slides | tool | abstract]

  5. André Platzer.
    Differential-algebraic dynamic logic for differential-algebraic programs.
    Journal of Logic and Computation, 20(1), pages 309-352, 2010. Advance Access published on November 18, 2008 by Oxford University Press.
    [bib | pdf | doi | study | abstract]

  6. André Platzer.
    Differential dynamic logic for hybrid systems.
    Journal of Automated Reasoning, 41(2), pages 143-189, 2008. © Springer-Verlag
    [bib | pdf | doi | study | abstract]

  7. André Platzer.
    Differential dynamic logic for verifying parametric hybrid systems.
    In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, volume 4548 of LNCS, pages 216-232. Springer, 2007. © Springer-Verlag
    This paper was awarded the TABLEAUX Best Paper Award.
    [bib | pdf | doi | slides | study | TR | abstract]