Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Automated Theory Exploration for Interactive Theorem Proving: Read chapter Read first chapter

2017 | Supplement | Chapter

Bellerophon: Tactical Theorem Proving for Hybrid Systems

Authors : Nathan Fulton, Stefan Mitsch, Rose Bohrer, André Platzer

Published in: Interactive Theorem Proving

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq
next chapter Formalizing Basic Quaternionic Analysis
Footnotes
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
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
The addressing scheme extends to subformulas and subterms in a straight-forward way. Interested readers may refer to the Bellerophon documentation for details.
 
4
Tactic e is applicable at a position pos if e(pos) does not result in an error.
 
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
Advanced automation generally uses the EDSL. Programs written in the EDSL are executed using the same interpreter as programs written in pure Bellerophon.
 
Literature
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_​26CrossRef
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
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_​29CrossRef
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)
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)MathSciNetCrossRef
6.
Chlipala, A.: Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)MATH
7.
Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299–328 (1991)MathSciNetCrossRef
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)
9.
Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1/2), 29–35 (1988)MathSciNetCrossRef
10.
Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. STTT 10(3), 263–279 (2008)CrossRef
11.
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_​36CrossRef
13.
14.
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_​19CrossRef
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_​21CrossRef
17.
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_​15CrossRef
19.
Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Log. Methods Comput. Sci. 9(1) (2011)
20.
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)
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’14CrossRef
23.
24.
25.
26.
Platzer, A.: Logics of dynamical systems. In: LICS. pp. 13–24. IEEE (2012)
27.
Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219–266 (2017)MathSciNetCrossRef
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’08CrossRef
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_​15CrossRef
30.
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_​26CrossRef
Metadata
Title
Bellerophon: Tactical Theorem Proving for Hybrid Systems
Authors
Nathan Fulton
Stefan Mitsch
Rose Bohrer
André Platzer
Copyright Year
2017
Publisher
Springer International Publishing
Book
Interactive Theorem Proving

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

Electronic ISBN: 978-3-319-66107-0

Copyright Year: 2017

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

Premium Partner

    Image Credits