The work summarized here is supported by JSPS Grants-in-Aid No. 24680001, 24800035, 25730040 & 15KT0012; Aihara Innovative Mathematical Modelling Project, FIRST Program, JSPS/CSTP; and JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Alur, R., et al.: The algorithmic analysis of hybrid systems. Theor. Comp. Sci. 138(1), 3–34 (1995)
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). http://doi.acm.org/10.1145/512950.512973
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). https://doi.org/10.1007/978-94-011-1793-7_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). https://doi.org/10.1007/978-3-642-31424-7_34
Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292. IEEE Computer Society (1996)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580, 583 (1969)
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). https://doi.org/10.1007/978-3-662-49122-5_11
Platzer, A.: Logical Analysis of Hybrid Systems-Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14509-4
Robinson, A.: Non-standard Analysis. Princeton University Press, Princeton (1996)
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). https://doi.org/10.1007/978-3-642-22012-8_31
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)
Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Hasuo, I. (2019). Nonstandard Static Analysis: Literal Transfer of Deductive Verification Frameworks from Discrete to Hybrid. In: Chamberlain, R., Taha, W., Törngren, M. (eds) Cyber Physical Systems. Design, Modeling, and Evaluation. CyPhy 2017. Lecture Notes in Computer Science(), vol 11267. Springer, Cham. https://doi.org/10.1007/978-3-030-17910-6_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-17910-6_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-17909-0
Online ISBN: 978-3-030-17910-6
eBook Packages: Computer ScienceComputer Science (R0)