Skip to main content
SpringerLink
Log in

Bellerophon: Tactical Theorem Proving for Hybrid Systems

  • Conference paper
Interactive Theorem Proving (ITP 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10499))

Included in the following conference series:

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 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.

This material is based upon work supported by the National Science Foundation under NSF CAREER Award CNS-1054246 and NSF CNS-1446712. This research was sponsored by the AFOSR under grant number FA9550-16-1-0288. This research was supported as part of the Future of Life Institute (futureoflife.org) FLI-RFP-AI1 program, grant #2015-143867.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    A continuous evolution along the differential equation system \(x_i'=\theta _i\) for an arbitrary duration within the region described by formula F. The & F is optional so that e.g., \(\{x'=\theta \}\) is equivalent to \( \{x'=\theta \& \textit{true}\}\).

  2. 2.

    Tactics may map a single sequent to a list of sequents; the simplest example of such a tactic andR corresponds to the proof rule \(\wedge \text {R}\), which maps a single sequent \(\varGamma \vdash A \wedge B, \varDelta \) to the list of subgoals \(\varGamma \vdash A, \varDelta \) and \(\varGamma \vdash B, \varDelta \).

  3. 3.

    The addressing scheme extends to subformulas and subterms in a straight-forward way. Interested readers may refer to the Bellerophon documentation for details.

  4. 4.

    Tactic e is applicable at a position pos if e(pos) does not result in an error.

  5. 5.

    The attentive reader will notice we use g() instead of g. This is to indicate that the model has an arity 0 function symbol g(), rather than an assignable variable. This syntactic convention follows KeYmaera X and its predecessors.

  6. 6.

    Advanced automation generally uses the EDSL. Programs written in the EDSL are executed using the same interpreter as programs written in pure Bellerophon.

References

  1. de Moura, L.M., Kong, S., Avigad, J., Doorn, F., Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 378–388. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_26

    Chapter  Google Scholar 

  2. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., et al. (eds.) [13], pp. 209–229

    Google Scholar 

  3. Barras, B., Carmen González Huesca, L., Herbelin, H., Régis-Gianas, Y., Tassi, E., Wenzel, M., Wolff, B.: Pervasive parallelism in highly-trustable interactive theorem proving systems. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 359–363. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39320-4_29

    Chapter  Google Scholar 

  4. Bohrer, R., Rahli, V., Vukotic, I., Völp, M., Platzer, A.: Formally verified differential dynamic logic. In: Certified Programs and Proofs - 6th ACM SIGPLAN Conference, CPP 2017, pp. 208–221. ACM (2017)

    Google Scholar 

  5. Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015)

    Article  MathSciNet  Google Scholar 

  6. Chlipala, A.: Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)

    MATH  Google Scholar 

  7. Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299–328 (1991)

    Article  MathSciNet  Google Scholar 

  8. Constable, R.L., Allen, S.F., Bromley, M., et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Upper Saddle River (1986)

    Google Scholar 

  9. Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1/2), 29–35 (1988)

    Article  MathSciNet  Google Scholar 

  10. Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. STTT 10(3), 263–279 (2008)

    Article  Google Scholar 

  11. Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_30

    Chapter  Google Scholar 

  12. Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 527–538. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_36

    Chapter  Google Scholar 

  13. Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.): Hybrid Systems. LNCS, vol. 736. Springer, Heidelberg (1993). doi:10.1007/3-540-57318-6

    Book  Google Scholar 

  14. Harrison, J.: A HOL theory of euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114–129. Springer, Heidelberg (2005). doi:10.1007/11541868_8

    Chapter  Google Scholar 

  15. Hickey, J., et al.: MetaPRL – a modular logical environment. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 287–303. Springer, Heidelberg (2003). doi:10.1007/10930755_19

    Chapter  Google Scholar 

  16. Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 279–294. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39634-2_21

    Chapter  Google Scholar 

  17. Immler, F., Traut, C.: The flow of ODEs. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 184–199. Springer, Cham (2016). doi:10.1007/978-3-319-43144-4_12

    Chapter  Google Scholar 

  18. Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_15

    Chapter  Google Scholar 

  19. Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Log. Methods Comput. Sci. 9(1) (2011)

    Google Scholar 

  20. The Coq Development Team: The Coq proof assistant reference manual. LogiCal Project (2004). http://coq.inria.fr, version 8.0

  21. Mitsch, S., Platzer, A.: The KeYmaera X proof IDE: concepts on usability in hybrid systems theorem proving. In: FIDE-3. EPTCS, vol. 240, pp. 67–81 (2016)

    Google Scholar 

  22. Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. Form. Methods Syst. Des. 49(1), 33–74 (2016). Special issue of selected papers from RV’14

    Article  Google Scholar 

  23. Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). doi:10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  24. Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143–189 (2008)

    Article  MathSciNet  Google Scholar 

  25. Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14509-4

    Book  MATH  Google Scholar 

  26. Platzer, A.: Logics of dynamical systems. In: LICS. pp. 13–24. IEEE (2012)

    Google Scholar 

  27. Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219–266 (2017)

    Article  MathSciNet  Google Scholar 

  28. Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. Form. Methods Syst. Des. 35(1), 98–120 (2009). Special issue for selected papers from CAV’08

    Article  Google Scholar 

  29. Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 171–178. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71070-7_15

    Chapter  Google Scholar 

  30. Platzer, A., Quesel, J.-D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 485–501. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02959-2_35

    Chapter  Google Scholar 

  31. Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 383–397. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38088-4_26

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

    Nathan Fulton, Stefan Mitsch, Rose Bohrer & André Platzer

Authors
  1. Nathan Fulton
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Mitsch
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rose Bohrer
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. André Platzer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nathan Fulton .

Editor information

Editors and Affiliations

  1. University of Brasília, Brasília D.F., Brazil

    Mauricio Ayala-Rincón

  2. NASA, Hampton, VA, USA

    César A. Muñoz

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Fulton, N., Mitsch, S., Bohrer, R., Platzer, A. (2017). Bellerophon: Tactical Theorem Proving for Hybrid Systems. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66107-0_14

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66106-3

  • Online ISBN: 978-3-319-66107-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation