The KeYmaera X Theorem Prover for Hybrid Systems

Download
pdf

Abstract:

KeYmaera X is a theorem prover for specifying and verifying correctness properties of hybrid systems (systems that mix discrete and continuous dynamics). KeYmaera X implements differential dynamic logic (dL) and provides a high degree of control over automated proof search.

  • Carnegie Mellon University
  • hybrid systems
  • Logical Systems Lab
  • Architectures
  • CPS Domains
  • Control
  • Validation and Verification
  • CPS Technologies
  • Foundations
  • National CPS PI Meeting 2015
  • 2015
  • Abstract
  • Poster
  • Academia
  • 2015 CPS PI MTG Videos, Posters, and Abstracts
Submitted by Bruce Krogh on