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:
Static Analysis of Non-interference in Expressive Low-Level Languages Read chapter Read first chapter

2015 | OriginalPaper | Chapter

A Simple Abstraction of Arrays and Maps by Program Translation

Authors : David Monniaux, Francesco Alberti

Published in: Static Analysis

Publisher: Springer Berlin Heidelberg

Log in

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

search-config
loading …

Abstract

We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar operations. The simplest way to implement it is by automatic, syntactic transformation of the array program into a scalar program followed analysis of the scalar program with any static analysis technique (abstract interpretation, acceleration, predicate abstraction,...). The scalars invariants thus obtained are translated back onto the original program as universally quantified array invariants. We illustrate our approach on a variety of examples, leading to the “Dutch flag” algorithm.

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 Refinement Type Inference via Horn Constraint Optimization
next chapter Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization
Footnotes
2
Possible since Astrée targets safety-critical embedded systems where array sizes are typically fixed at system design and dynamic memory allocation is prohibited.
 
3
We have left out, for the sake of brevity, tests for array accesses out of bounds.
 
4
We implemented a simplification algorithm for quantifier-free Presburger arithmetic inspired by [37] so as to understand the output of Flata and ConcurInterproc.
 
6
scripts/cpa.sh -predicateAnalysis after preprocessing with assert.h.
 
7
All timings using one core of a 2.4 GHz Intel ® Core™ i3 running 32-bit Linux.
 
11
From Presburger arithmetic, a decidable theory.
 
Literature
1.
Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 15–30. Springer, Heidelberg (2014) CrossRef
2.
Alberti, F., et al.: An extension of lazy abstraction with interpolation for programs with arrays. Form. Methods Syst. Des. 45(1), 63–109 (2014)CrossRefMATH
3.
Alberti, F., Ghilardi, S., Sharygina, N.: Definability of accelerated relations in a theory of arrays and its applications. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 23–39. Springer, Heidelberg (2013) CrossRef
4.
Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. J. Autom. Reasoning 54(4), 327–352 (2015)MathSciNetCrossRef
5.
Alberti, F., Monniaux, D.: Polyhedra to the rescue of array interpolants. In: Symposium on applied computing (Software Verification & Testing). ACM (2015)
6.
Bjørner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 105–125. Springer, Heidelberg (2013) CrossRef
7.
Blanchet, et al.: A static analyzer for large safety-critical software. In: PLDI, pp. 196–207. ACM (2003)
8.
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002) CrossRef
9.
Bozga, M., Habermehl, P., Iosif, R., Konečný, F., Vojnar, T.: Automatic verification of integer array programs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 157–172. Springer, Heidelberg (2009) CrossRef
10.
Bozga, M., Iosif, R., Konečný, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227–242. Springer, Heidelberg (2010) CrossRef
11.
Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundamenta Informaticae 91, 275–303 (2009)MathSciNetMATH
12.
13.
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84–96 (1978)
14.
Cousot, P., Cousot, R.: Invited talk: Higher order abstract interpretation. In: IEEE International Conference on Computer Languages, pp. 95–112. IEEE Computer Society (1994)
15.
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does Astrée scale up? Form. Methods Syst. Des. 35(3), 229–264 (2009)CrossRefMATH
16.
Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL, pp. 105–118. ACM (2011)
17.
Cox, A., Chang, B.-Y.E., Rival, X.: Automatic analysis of open objects in dynamic language programs. In: Müller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 134–150. Springer, Heidelberg (2014)
18.
Dijkstra, E.W.: A discipline of programming. Prentice-Hall, Upper Saddle River (1976)MATH
19.
Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 246–266. Springer, Heidelberg (2010) CrossRef
20.
Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191–202 (2002)
21.
Gopan, D., Reps, T., Sagiv, S.: A framework for numeric analysis of array operations. In: POPL, pp. 338–350 (2005)
22.
23.
Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: PLDI, pp. 339–348. ACM (2008)
24.
Halpern, J.: Presburger arithmetic with unary predicates is \(\Pi ^1_1\) complete. J. Symbolic Log. 56(2), 637–642 (1991)CrossRefMATH
25.
Hoder, K., Kovács, L., Voronkov, A.: Invariant generation in vampire. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 60–64. Springer, Heidelberg (2011) CrossRef
26.
Hoder, K., Kovács, L., Voronkov, A.: Interpolation and symbol elimination in vampire. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 188–195. Springer, Heidelberg (2010) CrossRef
27.
Hojjat, H., Konečný, F., Garnier, F., Iosif, R., Kuncak, V., Rümmer, P.: A verification toolkit for numerical transition systems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 247–251. Springer, Heidelberg (2012) CrossRef
28.
Jeannet, B., Gopan, D., Reps, T.: A relational abstraction for functions. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 186–202. Springer, Heidelberg (2005) CrossRef
29.
Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009) CrossRef
30.
Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007) CrossRef
31.
Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013) CrossRef
32.
McMillan, K.L.: Applications of craig interpolation to model checking. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 15–16. Springer, Heidelberg (2005) CrossRef
33.
McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413–427. Springer, Heidelberg (2008) CrossRef
34.
McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006) CrossRef
35.
McMillan, K.: Interpolants from Z3 proofs. In: FMCAD, pp. 19–27 (2011)
36.
Miné, A.: The octagon abstract domain. High. Order Symbolic Comput. 19(1), 31–100 (2006)CrossRefMATH
37.
Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243–257. Springer, Heidelberg (2008) CrossRef
38.
39.
40.
Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program Lang. Syst. 29(5), 26 (2007)CrossRef
Metadata
Title
A Simple Abstraction of Arrays and Maps by Program Translation
Authors
David Monniaux
Francesco Alberti
Copyright Year
2015
Publisher
Springer Berlin Heidelberg
Book
Static Analysis

Print ISBN: 978-3-662-48287-2

Electronic ISBN: 978-3-662-48288-9

Copyright Year: 2015

DOI
https://doi.org/10.1007/978-3-662-48288-9_13

Premium Partner

    Image Credits