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:
Automating Abstract Interpretation Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Abstract Interpretation with Infinitesimals

Towards Scalability in Nonstandard Static Analysis

Authors : Kengo Kido, Swarat Chaudhuri, Ichiro Hasuo

Published in: Verification, Model Checking, and Abstract Interpretation

Publisher: Springer Berlin Heidelberg

Log in

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

search-config
loading …

Abstract

We extend abstract interpretation for the purpose of verifying hybrid systems. Abstraction has been playing an important role in many verification methodologies for hybrid systems, but some special care is needed for abstraction of continuous dynamics defined by ODEs. We apply Cousot and Cousot’s framework of abstract interpretation to hybrid systems, almost as it is, by regarding continuous dynamics as an infinite iteration of infinitesimal discrete jumps. This extension follows the recent line of work by Suenaga, Hasuo and Sekine, where deductive verification is extended for hybrid systems by (1) introducing a constant \(\mathtt {dt}\) for an infinitesimal value; and (2) employing Robinson’s nonstandard analysis (NSA) to define mathematically rigorous semantics. Our theoretical results include soundness and termination via uniform widening operators; and our prototype implementation successfully verifies some benchmark examples.

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 Exact Heap Summaries for Symbolic Execution
next chapter Lipschitz Robustness of Timed I/O Systems
Footnotes
2
There are also examples in which discretization even leads to unsound analysis results.
 
3
The name “standard” is confusing with the distinction between standard and nonstandard entities in NSA. The use of “standard” in the former sense is scarce in this paper.
 
4
If we interpret commands as functions \( {\mathcal P}(\mathbf {Var}\rightarrow {}^{*}{}{\mathbb {R}}) \rightarrow {\mathcal P}(\mathbf {Var}\rightarrow {}^{*}{}{\mathbb {R}})\), the interpretation \(\llbracket \mathtt {while}\; x<10 \;\mathtt {do}\; x:= x+\mathtt {dt} \rrbracket \{(x\mapsto 0)\}\) by a least fixed point will be \(\{x\mapsto r \mid \exists n \in \mathbb {N}.\; r = n*\mathtt {dt}\}\), not \(\{x\mapsto r \mid \exists n \in {}^{*}{}{\mathbb {N}}.\; r = n*\mathtt {dt}\wedge r\le 10\}\) as we expect. The problem is that internality—an “well-behavedness” notion in NSA—is not preserved in such a modeling.
 
5
One can see that the ascending chain defined by \(X_n := \{k*\mathtt {dt}\mid 0\le k \le n\}\) does not have the supremum in \({}^{*}{}{{\mathcal P}}(\mathbb {R}^n)\) since \(\{k*\mathtt {dt}\mid k\in \mathbb {N}\}\) is not internal (see [28, Appendix A]).
 
6
Recall that \(\textsc {While}^{\mathtt {dt}}\) is a modeling language and we do not execute them.
 
Literature
1.
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736. Springer, Heidelberg (1993)CrossRef
2.
Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)MathSciNetCrossRef
3.
Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1–2), 28–56 (2005)MATHMathSciNetCrossRef
4.
Beauxis, R., Mimram, S.: A non-standard semantics for Kahn networks in continuous time. In: CSL, pp. 35–50 (2011)
5.
Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013)CrossRef
6.
Chernikova, N.: Algorithm for finding a general formula for the non-negative solutions of a system of linear equations. USSR Comput. Math. Math. Phys. 4(4), 151–158 (1964)CrossRef
7.
Chernikova, N.: Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities. USSR Comput. Math. Math. Phys. 5(2), 228–233 (1965)MathSciNetCrossRef
8.
Chernikova, N.: Algorithm for discovering the set of all the solutions of a linear programming problem. USSR Comput. Math. Math. Phys. 8(6), 282–293 (1968)CrossRef
9.
Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, chap. 10, pp. 303–342. Prentice-Hall Inc, Englewood Cliffs, New Jersey (1981)
10.
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977. pp. 238–252 (1977)
11.
12.
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)CrossRef
13.
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 84–96 (1978)
14.
Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)CrossRef
15.
Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT 1(3–4), 209–236 (2007)
16.
Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)CrossRef
17.
Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)CrossRef
18.
Goldblatt, R.: Lectures on the Hyperreals: An Introduction to Nonstandard Analysis. Graduate Texts in Mathematics. Springer, New York (1998)MATHCrossRef
19.
Halbwachs, N.: Determination automatique de relations linaires vrifiespar les variables d’un programme. Thse de 3e cycle, Universit Scientifique et Mdicale de Grenoble (1979)
20.
Halbwachs, N.: Delay analysis in synchronous programs. In: Proceedings of 5th International Conference on Computer Aided Verification, CAV 1993, Elounda, Greece, 28 June - 1 July 1993, pp. 333–346 (1993)
21.
Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods Syst. Des. 11(2), 157–185 (1997)CrossRef
22.
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)CrossRef
23.
24.
Henzinger, T.A., Ho, P.: Algorithmic analysis of nonlinear hybrid systems. In: Proceedings of 7th International Conference Computer Aided Verification, Liège, Belgium, 3–5 July 1995, pp. 225–238 (1995)
25.
Henzinger, T.A., Ho, P., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. STTT 1(1–2), 110–122 (1997)MATHCrossRef
26.
Hurd, A., Loeb, P.: An Introduction to Nonstandard Real Analysis. Pure and Applied Mathematics. Elsevier Science, New York (1985)MATH
27.
Kido, K.: An Alternative Denotational Semantics for an Imperative Language with Infinitesimals. Bachelor’s thesis, The University of Tokyo: Japan (2013)
28.
Kido, K., Chaudhuri, S., Hasuo, I.: Abstract interpretation with infinitesimals–towards scalability in nonstandard static analysis (2015). extended version with appendices http://​arxiv.​org/​
29.
30.
Le Verge, H.: A note on Chernikova’s Algorithm. Technical report 635, IRISA, Rennes, France, Febuary 1992
31.
Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)CrossRef
32.
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)CrossRef
33.
Robinson, A.: Non-standard Analysis. Studies in logic and the foundations of mathematics. North-Holland Pub. Co., Amsterdam (1966)MATH
34.
Suenaga, K., Hasuo, I.: Programming with Infinitesimals: A While-Language for Hybrid System Modeling. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 392–403. Springer, Heidelberg (2011)CrossRef
35.
Suenaga, K., Sekine, H., Hasuo, I.: Hyperstream processing systems: nonstandard modeling of continuous-time signals. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 23–25 January 2013, pp. 417–430 (2013)
36.
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)MATH
Metadata
Title
Abstract Interpretation with Infinitesimals
Authors
Kengo Kido
Swarat Chaudhuri
Ichiro Hasuo
Copyright Year
2016
Publisher
Springer Berlin Heidelberg
Book
Verification, Model Checking, and Abstract Interpretation

Print ISBN: 978-3-662-49121-8

Electronic ISBN: 978-3-662-49122-5

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-662-49122-5_11

Premium Partner

    Image Credits