Nonstandard Static Analysis: Literal Transfer of Deductive Verification Frameworks from Discrete to Hybrid

  • Ichiro HasuoEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11267)


The talk summarizes our series of work [4, 7, 10, 11]. Special thanks are due to my collaborators: Kohei Suenaga (Kyoto University), Swarat Chaudhuri (Rice University), and my (former) students Kengo Kido and Hiroyoshi Sekine (The University of Tokyo).


  1. 1.
    Alur, R., et al.: The algorithmic analysis of hybrid systems. Theor. Comp. Sci. 138(1), 3–34 (1995)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238–252. ACM (1977).
  3. 3.
    Floyd, R.W.: Assigning meanings to programs. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds.) Program Verification: Fundamental Issues in Computer Science. Studies in Cognitive Systems, vol. 14, pp. 65–81. Springer, Dordrecht (1993). Scholar
  4. 4.
    Hasuo, I., Suenaga, K.: Exercises in Nonstandard Static Analysis of hybrid systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 462–478. Springer, Heidelberg (2012). Scholar
  5. 5.
    Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292. IEEE Computer Society (1996)Google Scholar
  6. 6.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580, 583 (1969)CrossRefGoogle Scholar
  7. 7.
    Kido, K., Chaudhuri, S., Hasuo, I.: Abstract interpretation with infinitesimals. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 229–249. Springer, Heidelberg (2016). Scholar
  8. 8.
    Platzer, A.: Logical Analysis of Hybrid Systems-Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). Scholar
  9. 9.
    Robinson, A.: Non-standard Analysis. Princeton University Press, Princeton (1996)CrossRefGoogle Scholar
  10. 10.
    Suenaga, K., Hasuo, I.: Programming with infinitesimals: a While-language for hybrid system modeling. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 392–403. Springer, Heidelberg (2011). Scholar
  11. 11.
    Suenaga, K., Sekine, H., Hasuo, I.: Hyperstream processing systems: nonstandard modeling of continuous-time signals. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 417–430. ACM (2013)Google Scholar
  12. 12.
    Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.National Institute of InformaticsTokyoJapan
  2. 2.The Graduate University for Advanced Studies (SOKENDAI)TokyoJapan

Personalised recommendations