Pegasus: A Framework for Sound Continuous Invariant Generation

  • Andrew SogokonEmail author
  • Stefan MitschEmail author
  • Yong Kiam TanEmail author
  • Katherine CordwellEmail author
  • André PlatzerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)


Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to automation of formal proofs of safety in hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.


Invariant generation Continuous invariants Ordinary differential equations Theorem proving 



The authors would like to thank the anonymous reviewers for their feedback.


  1. 1.
    Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000). Scholar
  2. 2.
    Arrowsmith, D., Place, C.M.: Dynamical Systems: Differential Equations, Maps, and Chaotic Behaviour, vol. 5. CRC Press, Boca Raton (1992)CrossRefGoogle Scholar
  3. 3.
    Beckert, B., et al.: The KeY system 1.0 (deduction component). In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 379–384. Springer, Heidelberg (2007). Scholar
  4. 4.
    Sassi, M.A.B., Girard, A., Sankaranarayanan, S.: Iterative computation of polyhedral invariants sets for polynomial dynamical systems. In: CDC 2014, pp. 6348–6353. IEEE (2014).
  5. 5.
    Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179–194. Springer, Heidelberg (2010). Scholar
  6. 6.
    Bohrer, B., Tan, Y.K., Mitsch, S., Myreen, M.O., Platzer, A.: VeriPhy: verified controller executables from verified cyber-physical system models. In: Foster, J.S., Grossman, D. (eds.) PLDI 2018, pp. 617–630. ACM (2018).
  7. 7.
    Chen, M., et al.: MARS: a toolchain for modelling, analysis and verification of hybrid systems. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE 2017, pp. 39–58. Springer, Cham (2017).
  8. 8.
    Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). Scholar
  9. 9.
    Cox, D.A., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms. UTM 2015. Springer, Cham (2015).
  10. 10.
    Dai, L., Gan, T., Xia, B., Zhan, N.: Barrier certificates revisited. J. Symb. Comput. 80, 62–86 (2017). Scholar
  11. 11.
    Darboux, J.G.: Mémoire sur les équations différentielles algébriques du premier ordre et du premier degré. Bull. Sci. Math. 2(1), 151–200 (1878)zbMATHGoogle Scholar
  12. 12.
    Denman, W., Muñoz, C.: Automated real proving in PVS via MetiTarski. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 194–199. Springer, Cham (2014). Scholar
  13. 13.
    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). Scholar
  14. 14.
    Fulton, N., Mitsch, S., Bohrer, B., Platzer, A.: Bellerophon: tactical theorem proving for hybrid systems. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 207–224. Springer, Cham (2017). Scholar
  15. 15.
    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 (LNAI), vol. 9195, pp. 527–538. Springer, Cham (2015). Scholar
  16. 16.
    Gan, T., Chen, M., Li, Y., Xia, B., Zhan, N.: Reachability analysis for solvable dynamical systems. IEEE Trans. Autom. Control 63(7), 2003–2018 (2018). Scholar
  17. 17.
    Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 279–294. Springer, Heidelberg (2014). Scholar
  18. 18.
    Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Comput. Lang. Syst. Struct. 47, 19–43 (2017). Scholar
  19. 19.
    Goriely, A.: Integrability and Nonintegrability of Dynamical Systems. World Scientific, Hackensack (2001). Scholar
  20. 20.
    Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190–203. Springer, Heidelberg (2008). Scholar
  21. 21.
    Herbrand, J.: Recherches sur la théorie de la démonstration. Ph.D. thesis, Université de Paris, Faculté des Sciences (1930)Google Scholar
  22. 22.
    Immler, F., et al.: ARCH-COMP18 category report: continuous and hybrid systems with nonlinear dynamics. In: Frehse, G., Althoff, M., Bogomolov, S., Johnson, T.T. (eds.) ARCH 2018. EPiC Series in Computing, vol. 54, pp. 53–70. EasyChair (2018)Google Scholar
  23. 23.
    Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., Arechiga, N.: Simulation-guided Lyapunov analysis for hybrid dynamical systems. In: Fränzle, M., Lygeros, J. (eds.) HSCC 2014, pp. 133–142. ACM (2014).
  24. 24.
    Kong, H., Bogomolov, S., Schilling, C., Jiang, Y., Henzinger, T.A.: Safety verification of nonlinear hybrid systems based on invariant clusters. In: Frehse, G., Mitra, S. (eds.) HSCC 2017, pp. 163–172. ACM (2017).
  25. 25.
    Kong, H., He, F., Song, X., Hung, W.N.N., Gu, M.: Exponential-Condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 242–257. Springer, Heidelberg (2013). Scholar
  26. 26.
    Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32(3), 231–253 (2001). Scholar
  27. 27.
    Li, W., Passmore, G.O., Paulson, L.C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. J. Autom. Reasoning 62(1), 69–91 (2019). Scholar
  28. 28.
    Liu, J., et al.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1–15. Springer, Heidelberg (2010). Scholar
  29. 29.
    Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT 2011, pp. 97–106. ACM (2011).
  30. 30.
    Loeser, T., Iwasaki, Y., Fikes, R.: Safety verification proofs for physical systems. In: Proceedings of the 12th International Workshop on Qualitative Reasoning, pp. 88–95 (1998)Google Scholar
  31. 31.
    Man, Y.: Computing closed form solutions of first order ODEs using the Prelle-Singer procedure. J. Symb. Comput. 16(5), 423–443 (1993). Scholar
  32. 32.
    Mishra, B.: Algorithmic Algebra. Springer, Cham (1993). Scholar
  33. 33.
    Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 49(1–2), 33–74 (2016). Scholar
  34. 34.
    Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143–189 (2008)MathSciNetCrossRefGoogle Scholar
  35. 35.
    Platzer, A.: The complete proof theory of hybrid systems. In: LICS 2012, pp. 541–550. IEEE (2012).
  36. 36.
    Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. Formal Methods Syst. Des. 35(1), 98–120 (2009). Scholar
  37. 37.
    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 (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008). Scholar
  38. 38.
    Platzer, A., Quesel, J.-D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 485–501. Springer, Heidelberg (2009). Scholar
  39. 39.
    Platzer, A., Tan, Y.K.: Differential equation axiomatization: the impressive power of differential ghosts. In: Dawar, A., Grädel, E. (eds.) LICS 2018, pp. 819–828. ACM (2018).
  40. 40.
    Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004). Scholar
  41. 41.
    Prelle, M.J., Singer, M.F.: Elementary first integrals of differential equations. Trans. Am. Math. Soc. 279(1), 215–229 (1983)MathSciNetCrossRefGoogle Scholar
  42. 42.
    Rebiha, R., Moura, A.V., Matringe, N.: Generating invariants for non-linear hybrid systems. Theor. Comput. Sci. 594, 180–200 (2015). Scholar
  43. 43.
    Renegar, J.: Recent progress on the complexity of the decision problem for the reals. In: Goodman, J.E., Pollack, R., Steiger, W. (eds.) Discrete and Computational Geometry: Papers from the DIMACS Special Year, vol. 6, pp. 287–308. DIMACS/AMS (1990)Google Scholar
  44. 44.
    Rodríguez-Carbonell, E., Tiwari, A.: Generating polynomial invariants for hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 590–605. Springer, Heidelberg (2005). Scholar
  45. 45.
    Rouche, N., Habets, P., Laloy, M.: Stability Theory by Liapunov’s Direct Method. Applied Mathematical Sciences. Springer, Heidelberg (1977). Scholar
  46. 46.
    Roux, P., Voronin, Y., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants. Formal Methods Syst. Des. 53(2), 286–312 (2018). Scholar
  47. 47.
    Roy, M.F.: Basic algorithms in real algebraic geometry and their complexity: from Sturm’s theorem to the existential theory of reals. De Gruyter Expositions Math. 23, 1–67 (1996)MathSciNetzbMATHGoogle Scholar
  48. 48.
    Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: Johansson, K.H., Yi, W. (eds.) HSCC 2010, pp. 221–230. ACM (2010).
  49. 49.
    Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods Syst. Des. 32(1), 25–55 (2008). Scholar
  50. 50.
    Shults, B., Kuipers, B.: Proving properties of continuous systems: qualitative simulation and temporal logic. Artif. Intell. 92(1–2), 91–129 (1997). Scholar
  51. 51.
    Sogokon, A., Ghorbal, K., Jackson, P.B., Platzer, A.: A method for invariant generation for polynomial continuous systems. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 268–288. Springer, Heidelberg (2016). Scholar
  52. 52.
    Sogokon, A., Ghorbal, K., Johnson, T.T.: Non-linear continuous systems for safety verification. In: Frehse, G., Althoff, M. (eds.) ARCH 2016. EPiC Series in Computing, vol. 43, pp. 42–51. EasyChair (2016)Google Scholar
  53. 53.
    Sogokon, A., Ghorbal, K., Tan, Y.K., Platzer, A.: Vector barrier certificates and comparison systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 418–437. Springer, Cham (2018). Scholar
  54. 54.
    Strogatz, S.H.: Nonlinear Dynamics And Chaos. Studies in Nonlinearity. Westview Press, Boulder (2001)Google Scholar
  55. 55.
    Sturm, T., Tiwari, A.: Verification and synthesis using real quantifier elimination. In: Schost, É., Emiris, I.Z. (eds.) ISSAC 2011, pp. 329–336. ACM (2011).
  56. 56.
    Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 514–525. Springer, Heidelberg (2003). Scholar
  57. 57.
    Tiwari, A.: Abstractions for hybrid systems. Formal Methods Syst. Des. 32(1), 57–83 (2008). Scholar
  58. 58.
    Tiwari, A.: Generating box invariants. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 658–661. Springer, Heidelberg (2008). Scholar
  59. 59.
    Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 465–478. Springer, Heidelberg (2002). Scholar
  60. 60.
    Tiwari, A., Khanna, G.: Nonlinear systems: approximating reach sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 600–614. Springer, Heidelberg (2004). Scholar
  61. 61.
    Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382–399. Springer, Cham (2015). Scholar
  62. 62.
    Weber, T.: Integrating a SAT solver with an LCF-style theorem prover. Electron. Notes Theor. Comput. Sci. 144(2), 67–78 (2006). Scholar
  63. 63.
    Weber, T.: SMT solvers: new oracles for the HOL theorem prover. STTT 13(5), 419–429 (2011). Scholar
  64. 64.
    Yang, Z., Huang, C., Chen, X., Lin, W., Liu, Z.: A linear programming relaxation based approach for generating barrier certificates of hybrid systems. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 721–738. Springer, Cham (2016). Scholar
  65. 65.
    Zaki, M.H., Denman, W., Tahar, S., Bois, G.: Integrating abstraction techniques for formal verification of analog designs. J. Aeros. Comp. Inf. Com. 6(5), 373–392 (2009). Scholar
  66. 66.
    Zhao, F.: Extracting and representing qualitative behaviors of complex systems in phase space. Artif. Intell. 69(1–2), 51–92 (1994). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Computer Science DepartmentCarnegie Mellon UniversityPittsburghUSA
  2. 2.School of InformaticsUniversity of EdinburghEdinburghUK
  3. 3.Fakultät für InformatikTechnische Universität MünchenMünchenGermany

Personalised recommendations