[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Bounded underapproximations

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

Abstract

We show a new and constructive proof of the following language-theoretic result: for every context-free language L, there is a bounded context-free language L′⊆L which has the same Parikh (commutative) image as L. Bounded languages, introduced by Ginsburg and Spanier, are subsets of regular languages of the form \(w_{1}^{*}w_{2}^{*}\cdots w_{m}^{*}\) for some w 1,…,w m ∈Σ ∗. In particular bounded context-free languages have nice structural and decidability properties. Our proof proceeds in two parts. First, we give a new construction that shows that each context free language L has a subset L N that has the same Parikh image as L and that can be represented as a sequence of substitutions on a linear language. Second, we inductively construct a Parikh-equivalent bounded context-free subset of L N .

We show two applications of this result in model checking: to underapproximate the reachable state space of multithreaded procedural programs and to underapproximate the reachable state space of recursive counter programs. The bounded language constructed above provides a decidable underapproximation for the original problems. By iterating the construction, we get a semi-algorithm for the original problems that constructs a sequence of underapproximations such that no two underapproximations of the sequence can be compared. This provides a progress guarantee: every word w∈L is in some underapproximation of the sequence, and hence, a program bug is guaranteed to be found. In particular, we show that verification with bounded languages generalizes context-bounded reachability for multithreaded 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
£29.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 includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Algorithm 1
Algorithm 2
Fig. 1
Fig. 2

Similar content being viewed by others

Notes

  1. Σ={0,1} is ordered as 0≺1.

  2. The composition of two relations R 1 and R 2, denoted , is defined as the relation {(x,x 1)∣∃x′:R 1(x,x′)∧R 2(x′,x 1)}.

References

  1. Bardin S, Finkel A, Leroux J, Schnoebelen P (2005) Flat acceleration in symbolic model checking. In: ATVA ’05: proc 3rd int symp on automated technology for verification and analysis. LNCS, vol 3707. Springer, Berlin, pp 474–488

    Chapter  Google Scholar 

  2. Blattner M, Latteux M (1981) Parikh-bounded languages. In: ICALP ’81: proc of 8th int colloquium on automata, languages and programming. LNCS, vol 115. Springer, Berlin, pp 316–323

    Chapter  Google Scholar 

  3. Bouajjani A, Esparza J, Touili T (2003) A generic approach to the static analysis of concurrent programs with procedures. In: POPL ’03: proc 30th ACM SIGPLAN-SIGACT symp on principles of programming languages. ACM Press, New York, pp 62–73

    Chapter  Google Scholar 

  4. Bozga M, Gîrlea C, Iosif R (2009) Iterating octagons. In: TACAS ’09: proc 15th int conf on tools and algorithms for the construction and analysis of systems. LNCS, vol 5505. Springer, Berlin, pp 337–351

    Chapter  Google Scholar 

  5. Bozga M, Iosif R, Moro P, Vojnar T, Bouajjani A, Habermehl P (2006) Programs with lists are counter automata. In: CAV ’06: proc 18th int conf on computer aided verification. LNCS, vol 4144. Springer, Berlin, pp 517–531

    Google Scholar 

  6. Esparza J, Ganty P (2011) Complexity of pattern-based verification for multithreaded programs. In: POPL ’11: proc 38th ACM SIGACT-SIGPLAN symp on principles of programming languages. ACM Press, New York, pp 499–510

    Google Scholar 

  7. Esparza J, Ganty P, Kiefer S, Luttenberger M (2010) Parikh’s theorem: A simple and direct automaton construction. CoRR, abs/1006.3825

  8. Esparza J, Kiefer S, Luttenberger M (2008) Newton’s method for ω-continuous semirings. In: ICALP ’08: proc 35th int coll on automata, languages and programming. LNCS, vol 5126. Springer, Berlin, pp 14–26. Invited paper

    Chapter  Google Scholar 

  9. Esparza J, Kiefer S, Luttenberger M (2010) Newtonian program analysis. J ACM 57(6):331–3347

    Article  MathSciNet  Google Scholar 

  10. Finkel A, Leroux J (2002) How to compose Presburger-accelerations: applications to broadcast protocols. In: FSTTCS ’02: proc 22nd int conf on foundations of software technology and theoretical computer science. LNCS, vol 2556. Springer, Berlin, pp 145–156

    Google Scholar 

  11. Ganty P, Majumdar R, Monmege B (2010) Bounded underapproximations. In: CAV ’10: proc 20th int conf on computer aided verification. LNCS, vol 6174. Springer, Berlin, pp 600–614. See also CoRR report abs/0809.1236

    Chapter  Google Scholar 

  12. Ginsburg S (1966) The mathematical theory of context-free languages. McGraw-Hill, New York

    MATH  Google Scholar 

  13. Ginsburg S, Spanier EH (1964) Bounded ALGOL-like languages. Trans Am Math Soc 113(2):333–368

    MathSciNet  MATH  Google Scholar 

  14. Hague M, Lin AW (2011) Model checking recursive programs with numeric data types. In: CAV ’11: proc 21th int conf on computer aided verification. LNCS. Springer, Berlin

    Google Scholar 

  15. Harju T, Ibarra OH, Karhumäki J, Salomaa A (2002) Some decision problems concerning semilinearity and commutation. J Comput Syst Sci 65:278–294

    Article  MATH  Google Scholar 

  16. Hopcroft JE, Ullman JD (1979) Introduction to automata theory, languages and computation, 1st edn. Addison-Wesley, Reading

    MATH  Google Scholar 

  17. Kahlon V Tractable dataflow analysis for concurrent programs via bounded languages. Patent WO/2009/094439, July 2009

  18. Latteux M, Leguy J (1979) Une propriété de la famille GRE. In: FCT ’79: fundamentals of computation theory, Proc of the conf on algebraic, arithmetic, and categorial methods in computation theory. Akademie-Verlag, Berlin, pp 255–261

    Google Scholar 

  19. Leroux J, Sutre G (2004) On flatness for 2-dimensional vector addition systems with states. In: CONCUR ’04: proc 15th int conf on concurrency theory. LNCS, vol 3170. Springer, Berlin, pp 402–416

    Chapter  Google Scholar 

  20. Qadeer S, Rehof J (2005) Context-bounded model checking of concurrent software. In: TACAS ’05: proc 11th int conf on tools and algorithms for the construction and analysis of systems. LNCS, vol 3440. Springer, Berlin, pp 93–107

    Chapter  Google Scholar 

  21. Ramalingam G (2000) Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans Program Lang Syst 22(2):416–430

    Article  Google Scholar 

  22. Suwimonteerabuth D, Esparza J, Schwoon S (2008) Symbolic context-bounded analysis of multithreaded Java programs. In: SPIN’08: proc of 15th int model checking software workshop. LNCS, vol 5156. Springer, Berlin, pp 270–287

    Google Scholar 

  23. To AW (2010) Model checking infinite-state systems: generic and specific approaches. PhD thesis, School of Informatics, University of Edinburgh

  24. van Begin L (2003) Efficient verification of counting abstractions for parametric systems. PhD thesis, Université Libre de Bruxelles, Belgium

Download references

Acknowledgements

We thank Javier Esparza for his help on the lower bounds of Lemmas 8 and 13, respectively. We also thank Stefan Kiefer, Michael Luttenberger, and Zhenyue Long for helpful discussions, and the anonymous referees who gave relevant comments which helped in improving the paper. Finally, we thank Michael Emmi for the example of Fig. 1.

Author information

Authors and Affiliations

  1. IMDEA Software, Facultad de Informática (UPM), Campus Montegancedo, 28660-Boadilla del Monte, Madrid, Spain

    Pierre Ganty

  2. MPI-SWS, Gottlieb-Daimler-Strasse Building 49, 67663, Kaiserslautern, Germany

    Rupak Majumdar

  3. UC Los Angeles, Los Angeles, CA, USA

    Rupak Majumdar

  4. LSV, ENS Cachan, CNRS & INRIA, 61, avenue du Président Wilson, 94235, Cachan Cedex, France

    Benjamin Monmege

Authors
  1. Pierre Ganty
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rupak Majumdar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Benjamin Monmege
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Benjamin Monmege.

Additional information

This research was sponsored in part by the NSF grants CCF-0546170 and CCF-0702743, DARPA grant HR0011-09-1-0037, Comunidad de Madrid’s Program prometidos-cm (S2009TIC-1465), people-cofund’s program amarout (pcofund-2008-229599), and by the Spanish Ministry of Science and Innovation (tin2010-20639).

Rights and permissions

Reprints and permissions

About this article

Cite this article

Ganty, P., Majumdar, R. & Monmege, B. Bounded underapproximations. Form Methods Syst Des 40, 206–231 (2012). https://doi.org/10.1007/s10703-011-0136-y

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-011-0136-y

Keywords

Search

Navigation