Bellerophon swMATH ID: 23943 Software Authors: Fulton, Nathan; Mitsch, Stefan; Bohrer, Brandon; Platzer, André Description: Bellerophon: tactical theorem proving for hybrid systems. 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.{par}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 automation 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’s support for invariant and arithmetic reasoning for a non-solvable system. Homepage: https://link.springer.com/chapter/10.1007%2F978-3-319-66107-0_14 Related Software: KeYmaera; KeYmaera X; SpaceEx; Isabelle/HOL; ModelPlex; dReach; Coquelicot; Coq; MetiTarski; VeriPhy; Orbital library; z3; PVS; Sostools; Transformer semantics; Quantales; Differential_Game_Logic; KAD; Algebraic_VCs; Kleene Algebra Cited in: 5 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Bellerophon: tactical theorem proving for hybrid systems. Zbl 1483.68191Fulton, Nathan; Mitsch, Stefan; Bohrer, Brandon; Platzer, André 2017 all top 5 Cited by 9 Authors 4 Platzer, André 3 Tan, Yong Kiam 2 Mitsch, Stefan 1 Bohrer, Brandon 1 Cordwell, Katherine 1 Fulton, Nathan 1 Huerta y Munive, Jonathan Julián 1 Sogokon, Andrew 1 Struth, Georg Cited in 3 Serials 1 Journal of Automated Reasoning 1 Formal Aspects of Computing 1 Formal Methods in System Design Cited in 4 Fields 5 Computer science (68-XX) 3 Systems theory; control (93-XX) 2 Ordinary differential equations (34-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year