Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

We propose a new automaton model, called quantified data automata (QDA) over words, that can model quantified invariants over linear data structures, and study their theory, including closure properties, canonical minimality, and decidability of emptiness. We build poly-time active learning algorithms for them, where the learner is allowed to query the teacher with membership and equivalence queries. In order to express invariants in decidable logics, we invent a decidable subclass of QDAs, called elastic QDAs, and show translations to decidable theories of arrays and lists. We also prove that every QDA has a unique minimally-over-approximating elastic QDA, showing a robust technique for abstracting QDA-expressible properties to the decidable fragments expressed by elastic QDAs. We then give an application of these theoretically sound and efficient active learning algorithms to program verification by building a passive learning framework that efficiently learns adequate quantified linear data structure invariants from samples obtained from dynamic executions for a class of programs.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Notes

  1. Index variables occur in the case of arrays and index into arrays.

  2. We make sure that the type of an interpretation (i.e., whether it is for formulas in the Array Property Fragment or in the decidable syntactic fragment of Strand) is always clear from the context.

  3. The benchmark suite and the source code of our implementation is available at http://www.cs.uiuc.edu/~madhu/cav13/.

References

  1. Alberti F, Bruttomesso R, Ghilardi S, Sharygina N (2012) SMT-based abstraction for arrays with interpolants. In: Madhusudan P, Seshia SA (eds) Computer Aided Verification—24th international conference, CAV 2012, Berkeley, July 7-13, 2012 Proceedings. Lecture notes in computer science, vol 7358. Springer, Berlin, pp 679–685

  2. Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: CAV, pp 548–562

  3. Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75(2):87–106

    Article  MATH  MathSciNet  Google Scholar 

  4. Bollig B, Katoen JP, Kern C, Leucker M, Neider D (2010) Piegdon, D.R.: libalf: The automata learning framework. In: CAV, Springer, Berlin, pp 360–364

  5. Bouajjani A, Dragoi C, Enea C, Sighireanu M (2012) Abstract domains for automated reasoning about list-manipulating programs with infinite data. In: Kuncak V, Rybalchenko A (eds) VMCAI. Lecture notes in computer science, vol 7148. Springer, Berlin, pp 1–22

  6. Bradley AR (2011) SAT-based model checking without unrolling. In: Jhala R, Schmidt DA (eds) VMCAI. Lecture notes in computer science, vol 6538. Springer, Berlin, pp 70–87

  7. Bradley AR, Manna Z, Sipma HB (2006) What’s decidable about arrays? In: Emerson EA, Namjoshi KS (eds) VMCAI. Lecture notes in computer science, vol 3855. Springer, Berlin, pp 427–442

  8. Cadar C, Dunbar D, Engler DR (2008) KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves R, van Renesse R (eds.) 8th USENIX symposium on operating systems design and implementation, OSDI 2008, Dec 8–10, USENIX Association, San Diego, pp 209–224. http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf

  9. Chen YF, Farzan A, Clarke EM, Tsay YK,Wang BY (2009) Learning minimal separating DFA’s for compositional verification. In: Kowalewski S, Philippou A (eds) TACAS. Lecture notes in computer science, vol 5505. Springer, Berlin, pp 31–45

  10. Chen YF, Wang BY (2012) Learning boolean functions incrementally. In: In: Madhusudan P, Seshia SA (eds) Computer Aided Verification—24th international conference, CAV 2012, Berkeley, July 7-13, 2012 Proceedings. Lecture notes in computer science, vol 7358. Springer, Berlin, pp 55–70

  11. Cobleigh JM, Giannakopoulou D, Pasareanu CS (2003) Learning assumptions for compositional verification. In: Garavel H, Hatcliff J (eds) TACAS. Lecture notes in computer science, vol 2619. Springer, Berlin, pp 331–346

  12. Distefano D, O’Hearn PW, Yang H (2006) A local shape analysis based on separation logic. In: Hermanns H, Palsberg J (eds.) Tools and algorithms for the construction and analysis of systems, 12th international conference, TACAS 2006 Held as Part of the joint European conferences on theory and practice of software, ETAPS 2006, Vienna, Austria, Mar 25– Apr 2. Lecture notes in computer science, vol 3920, Springer, Berlin, pp 287–302. Springer doi:10.1007/11691372_19

  13. Ernst MD, Czeisler A, Griswold WG, Notkin D (2000) Quickly detecting relevant program invariants. In: ICSE, pp 449–458

  14. Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for ESC/Java. In: Oliveira JN, Zave P (eds) FME. Lecture notes in computer science, vol 2021. Springer, Berlin, pp 500–517

  15. Garg P, Löding C, Madhusudan P, Neider D (2014) ICE: a robust framework for learning invariants. In: Biere A, Bloem R (eds) CAV. Lecture notes in computer science, vol 8559. Springer, Berlin, pp 69–87

  16. Garg P, Madhusudan P, Parlato G (2013) Quantified data automata on skinny trees: An abstract domain for lists. In: Logozzo F, Fähndrich M (eds) SAS. Lecture notes in computer science, vol 7935. Springer, Berlin, pp 172–193

  17. Gold EM (1967) Language identification in the limit. Inf Control 10(5):447–474

    Article  MATH  Google Scholar 

  18. Grädel E, Thomas W, Wilke T (eds) (2002) Automata, logics, and infinite games, vol 2500. Springer, Heidelberg

  19. Jhala R, McMillan KL (2007) Array abstractions from proofs. In: Damm W, Hermanns H (eds) CAV. Lecture notes in computer science, vol 4590, Springer, Heidelberg, pp 193–206

  20. Kearns MJ, Vazirani UV (1994) An introduction to computational learning theory. MIT Press, Cambridge

    Google Scholar 

  21. Khoussainov B, Nerode A (2001) Automata theory and its applications. Birkhauser, Boston

    Book  MATH  Google Scholar 

  22. Kohavi Z (1970) Switching and finite automata theory. McGraw-Hill, Blacklick

    MATH  Google Scholar 

  23. Kong S, Jung Y, David C, Wang BY, Yi K (2010) Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: APLAS, pp 328–343. Springer, Heidelberg

  24. Madhusudan P, Parlato G, Qiu X (2011) Decidable logics combining heap structures and data. In: Ball T, Sagiv M (eds.) POPL, pp 611–622. ACM, New York

  25. Madhusudan P, Qiu X (2011) Efficient decision procedures for heaps using STRAND. In: Yahav E (ed) SAS. Lecture notes in computer science, vol 6887. Springer, Berlin, pp 43–59

  26. Mai H, Pek E, Xue H, King ST, Madhusudan P (2013) Verifying security invariants in ExpressOS. In: V. Sarkar, R. Bodík (eds.) ASPLOS, pp 293–304. ACM, New York

  27. McMillan KL (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr., Senzi F (eds.) CAV. Lecture notes in computer science, vol. 2725, Springer, Berlin, pp 1–13

  28. McMillan KL (2008) Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction andanalysis of systems. 14th international conference, TACAS 2008, held as part of thejoint European conferences on theory and practice of software, ETAPS 2008, Budapest, Mar 29–Apr 6. Lecture notes in computer science, vol 4963. Springer, Berlin, pp 413–427

  29. de Moura LM, Bjørner N, (2007) Efficient E-matching for SMT solvers. In: Pfenning F (ed) CADE. Lecture notes in computer science,vol 4603. Springer, Berlin, pp 183–198

  30. de Moura, LM, Bjørner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction andanalysis of systems. 14th international conference, TACAS 2008, held as part of thejoint European conferences on theory and practice of software, ETAPS 2008, Budapest, Mar 29–Apr 6. Lecture notes in computer science, vol 4963. Springer, Berlin, pp 337–340

  31. Rivest RL, Schapire RE (1993) Inference of finite automata using homing sequences. Inf Comput 103(2):299–347

    Article  MATH  MathSciNet  Google Scholar 

  32. Sagiv S, Reps TW, Wilhelm R (2002) Parametric shape analysis via 3-valued logic. ACM Trans Progr Lang Syst 24(3):217–298

    Article  Google Scholar 

  33. Seghir MN, Podelski A, Wies T (2009) Abstraction refinement for quantified array assertions. In: Palsberg J, Su Z (eds) SAS. Lecture notes in computer science, vol 5673. Springer, Berlin, pp 3–18

  34. Sharma R, Nori AV, Aiken A (2012) Interpolants as classifiers. In: Madhusudan P, Seshia SA (eds) Computer Aided Verification—24th international conference, CAV 2012, Berkeley, July 7-13, 2012 Proceedings. Lecture notes in computer science, vol 7358. Springer, Berlin, pp 71–87

  35. Srivastava S, Gulwani S (2009) Program verification using templates over predicate abstraction. In: Hind M, Diwan A (eds.) PLDI, pp 223–234. ACM, New York

  36. Thomas W (1997) Languages, automata, and logic. In: Rozenberg G, Salomaa A (eds) Handbook of formal language theory, vol III. Springer, Heidelberg, pp 389–455

    Chapter  Google Scholar 

  37. Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, IEEE Computer Society, pp 332–344

Download references

Acknowledgments

We would like to thank Xiaokang Qiu, who was involved in early discussions on finding an automaton model for the decidable fragment of Strand. This work was partially supported by NSF CAREER award #0747041 and NSF Expeditions in Computing ExCAPE Award #1138994.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Illinois at Urbana-Champaign, 201 N. Goodwin Ave., Urbana, IL, 61801, USA

    Pranav Garg & P. Madhusudan

  2. Lehrstuhl für Informatik 7, RWTH Aachen University, 52056, Aachen, Germany

    Christof Löding & Daniel Neider

Authors
  1. Pranav Garg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christof Löding
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. P. Madhusudan
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Daniel Neider
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pranav Garg.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Garg, P., Löding, C., Madhusudan, P. et al. Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists. Form Methods Syst Des 47, 120–157 (2015). https://doi.org/10.1007/s10703-015-0231-6

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-015-0231-6

Keywords

Search

Navigation