Assured Autonomy Tools Portal
Continual Assurance of Learning-Enabled, Cyber-Physical Systems (LE-CPS)

Bellerophon: Tactical Theorem Proving for Hybrid Systems

Abstract

Hybrid systems combine discrete and continuous dynamics, which makes them attractive as models for systems that combine computer control with physical motion. Verification is undecidable for hybrid systems and challenging for many models and properties of practical interest. Thus, human interaction and insight are essential for verification. Interactive theorem provers seek to increase user productivity by allowing them to focus on those insights. We present a tactics language and library for hybrid systems verification, named Bellerophon, that provides a way to convey insights by programming hybrid systems proofs.

We demonstrate that in focusing on the important domain of hybrid systems verification, Bellerophon emerges with unique automation that provides a productive proving experience for hybrid systems from a small foundational prover core in the KeYmaera X prover. Among the automa- tion that emerges are tactics for decomposing hybrid systems, discovering and establishing invariants of nonlinear continuous systems, arithmetic simplifications to maximize the benefit of automated solvers and general- purpose heuristic proof search. Our presentation begins with syntax and semantics for the Bellerophon tactic combinator language, culminating in an example verification effort exploiting Bellerophon support for invariant and arithmetic reasoning for a non-solvable system.

Year of Publication
2017
Conference Name
ITP
Publisher
Springer
ISBN Number
978-3-319-66106-3
DOI
10.1007/978-3-319-66107-0_14