Skip to main content
SpringerLink
Log in

An Analysis of Permutations in Arrays

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5944))

Abstract

This paper is concerned with the synthesis of invariants in programs with arrays. More specifically, we consider properties concerning array contents up to a permutation. For instance, to prove a sorting procedure, one has to show that the result is sorted, but also that it is a permutation of the initial array. In order to analyze this kind of properties, we define an abstract interpretation working on multisets of values, and able to discover invariant equations about such multisets.

This work has been partially supported by the ASOPT project of the “Agence Nationale de la Recherche” of the French Ministry of Research.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information and Computation 104(1), 2–34 (1993); Preliminary version appears in the Proc. of 5th LICS (1990)

    Google Scholar 

  2. Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: 2nd Int. Symp. on Programming, Dunod, Paris (1976)

    Google Scholar 

  4. Cousot, P.: Verification by abstract interpretation. In: Dershowitz, N. (ed.) Proc. Int. Symp. on Verification – Theory & Practice – Honoring Zohar Manna’s 64th Birthday, Taormina, Italy, June 29-July 4, pp. 243–268. Springer, Berlin (2003)

    Google Scholar 

  5. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall Series in Automatic Computation (1976)

    Google Scholar 

  6. Dill, D.L.: Timing assumptions and verification of finite state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)

    Google Scholar 

  7. Dovier, A., Piazza, C., Rossi, G.: A uniform approach to constraint-solving for lists, multisets, compact lists, and sets. ACM TOCL 9(3) (May 2008)

    Google Scholar 

  8. Dor, N., Rodeh, M., Sagiv, M.: CCSV: towards a realistic tool for statically detecting all buffer overflows in C. In: ACM Conference on Programming Language Design and Implementation, PLDI 2003, San Diego, June 2003, pp. 155–167 (2003)

    Google Scholar 

  9. Dantsin, E., Voronkov, A.: A nondeterministic polynomial-time unification algorithm for bags, sets and trees. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 180–196. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  10. Edmonds, J., Karp, R.M.: Theoretical improvements in algorithmic efficiency for network flow problems. J. ACM 19(2), 248–264 (1972)

    Article  MATH  Google Scholar 

  11. Ford, L.R., Fulkerson, D.R.: Maximal flow through a network. Canadian Journal of Mathematics 8, 399–404 (1956)

    MATH  MathSciNet  Google Scholar 

  12. Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL 2002, pp. 191–202. ACM, New York (2002)

    Chapter  Google Scholar 

  13. Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Necula, G.C., Wadler, P. (eds.) POPL 2008, pp. 235–246. ACM, New York (2008)

    Chapter  Google Scholar 

  14. Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: Proc. of POPL 2005, Long Beach, CA, pp. 338–350 (2005)

    Google Scholar 

  15. Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: ACM Conference on Programming Language Design and Implementation, PLDI 2008, Tucson (Az.), June 2008, pp. 339–348 (2008)

    Google Scholar 

  16. Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 474–489. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  18. Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  19. Kovács, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: FASE 2009. LNCS, vol. 5503, pp. 470–485. Springer, Heidelberg (2009)

    Google Scholar 

  20. Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 135–147. Springer, Heidelberg (2004)

    Google Scholar 

  21. Lindstrom, G.: Scanning list structures without stacks or tag bits. Information Processing Letters 2(2), 47–51 (1973)

    Article  MathSciNet  Google Scholar 

  22. Loginov, A., Reps, T.W., Sagiv, M.: Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 261–279. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  23. Luckham, D.C., Suzuki, N.: Verification of array, record, and pointer operations in Pascal. ACM Trans. Program. Lang. Syst. 1(2), 226–244 (1979)

    Article  MATH  Google Scholar 

  24. Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, pp. 310–319. IEEE CS Press, Los Alamitos (2001)

    Google Scholar 

  25. Péron, M., Halbwachs, N.: An abstract domain extending Difference-Bound Matrices with disequality constraints. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 268–282. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: ACM Conference on Programming Language Design and Implementation, PLDI 2009, pp. 223–234 (2009)

    Google Scholar 

  27. Singh, D., Ibrahim, A.M., Yohanna, T., Singh, J.N.: An overview of the applications of multisets. Novi. Sad J. Math. 37(2), 73–92 (2007)

    MATH  MathSciNet  Google Scholar 

  28. Suzuki, N., Jefferson, D.: Verification decidability of Presburger array programs. J. ACM 27(1) (January 1980)

    Google Scholar 

  29. Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002)

    Article  Google Scholar 

  30. Schorr, H., Waite, W.: An efficient machine independent procedure for garbage collection in various list structures. Communications of the ACM 10(8), 501–506 (1967)

    Article  MATH  Google Scholar 

  31. Syropoulos, A.: Mathematics of multisets. In: Calude, C.S., Pun, G., Rozenberg, G., Salomaa, A. (eds.) Multiset Processing. LNCS, vol. 2235, pp. 347–358. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  32. Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 335–348. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  33. Wilhelm, R., Sagiv, S., Reps, T.W.: Shape analysis. In: Watt, D.A. (ed.) CC 2000. LNCS, vol. 1781, pp. 1–17. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Vérimag, Grenoble University, France

    Valentin Perrelle & Nicolas Halbwachs

Authors
  1. Valentin Perrelle
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicolas Halbwachs
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Facultad de Informatica (UPM), IMDEA Software, Campus Montegancedo, 28660 Boadilla del Monte, Madrid, Spain

    Gilles Barthe

  2. Facultad de Informatica (UPM), IMDEA Software and Technical University of Madrid, Campus Montegancedo, 28660 Boadilla del Monte, Madrid, Spain

    Manuel Hermenegildo

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Perrelle, V., Halbwachs, N. (2010). An Analysis of Permutations in Arrays. In: Barthe, G., Hermenegildo, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2010. Lecture Notes in Computer Science, vol 5944. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11319-2_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11319-2_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11318-5

  • Online ISBN: 978-3-642-11319-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation