Top

Published in:

2019 | OriginalPaper | Chapter

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

Author : Ichiro Hasuo

Published in: Cyber Physical Systems. Design, Modeling, and Evaluation

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

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

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

next chapter Local Descent for Temporal Logic Falsification of Cyber-Physical Systems

Alur, R., et al.: The algorithmic analysis of hybrid systems. Theor. Comp. Sci. 138(1), 3–34 (1995)MathSciNetCrossRef

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_4CrossRef

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_34CrossRef

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)CrossRef

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_11CrossRefMATH

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

Robinson, A.: Non-standard Analysis. Princeton University Press, Princeton (1996)CrossRef

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). https://doi.org/10.1007/978-3-642-22012-8_31CrossRefMATH

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)

12.

Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)MATH

Title: Nonstandard Static Analysis: Literal Transfer of Deductive Verification Frameworks from Discrete to Hybrid
Author: Ichiro Hasuo
Publisher: Springer International Publishing
Book: Cyber Physical Systems. Design, Modeling, and Evaluation
Print ISBN: 978-3-030-17909-0

Electronic ISBN: 978-3-030-17910-6

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-17910-6_1

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner