article

Bounded underapproximations

Authors:

Rupak Majumdar,

Benjamin MonmegeAuthors Info & Claims

Formal Methods in System Design, Volume 40, Issue 2

Pages 206 - 231

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

Published: 01 April 2012 Publication History

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 ₁, 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.

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.

[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.

[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.

[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.

[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.

[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.

[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.

[9]

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

[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.

[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.

[12]

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

[13]

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

[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.

[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.

[16]

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

[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.

[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.

[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.

[21]

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

Digital Library

[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.

[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.

Cited By

Abdulla PAtig MChen YDiep BHolík LRezine ARümmer P(2017)Flatten and conquer: a framework for efficient analysis of string constraintsACM SIGPLAN Notices10.1145/3140587.306238452:6(602-617)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062384
Abdulla PAtig MChen YDiep BHolík LRezine ARümmer PCohen AVechev M(2017)Flatten and conquer: a framework for efficient analysis of string constraintsProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3062341.3062384(602-617)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3062341.3062384
Ganty PIosif RKoneăźNý F(2017)Underapproximation of procedure summaries for integer programsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-016-0420-719:5(565-584)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1007/s10009-016-0420-7
Show More Cited By

Bounded underapproximations
1. Theory of computation
  1. Formal languages and automata theory

Recommendations

Bounded underapproximations
CAV'10: Proceedings of the 22nd international conference on Computer Aided Verification

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 ...
Descriptional complexity of bounded context-free languages

We investigate finite-turn pushdown automata (PDAs) from the point of view of descriptional complexity. It is known that such automata accept exactly the class of ultralinear context-free languages. Furthermore, the increase in size when converting ...
Decision Problems for Probabilistic Finite Automata on Bounded Languages
MFCS & CSL 2010 Satellite Workshops: Selected Papers

We show that several problems concerning probabilistic finite automata of a fixed dimension and a fixed number of letters for bounded cut-point and strict cut-point languages are algorithmically undecidable by a reduction of Hilbert's tenth problem. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Methods in System Design

Formal Methods in System Design Volume 40, Issue 2

April 2012

165 pages

ISSN:0925-9856

Issue’s Table of Contents

Copyright © Copyright © 2012 Springer Science+Business Media, LLC.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 April 2012

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Abdulla PAtig MChen YDiep BHolík LRezine ARümmer P(2017)Flatten and conquer: a framework for efficient analysis of string constraintsACM SIGPLAN Notices10.1145/3140587.306238452:6(602-617)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062384
Abdulla PAtig MChen YDiep BHolík LRezine ARümmer PCohen AVechev M(2017)Flatten and conquer: a framework for efficient analysis of string constraintsProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3062341.3062384(602-617)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3062341.3062384
Ganty PIosif RKoneăźNý F(2017)Underapproximation of procedure summaries for integer programsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-016-0420-719:5(565-584)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1007/s10009-016-0420-7
(2016)Forward analysis and model checking for trace bounded WSTSTheoretical Computer Science10.1016/j.tcs.2016.04.020637:C(1-29)Online publication date: 18-Jul-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.04.020
Atig MNarayan Kumar KSaivasan P(2016)Acceleration in Multi-PushDown SystemsProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_45(698-714)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49674-9_45
Esparza JGanty PPoch T(2014)Pattern-Based Verification for Multithreaded ProgramsACM Transactions on Programming Languages and Systems10.1145/262964436:3(1-29)Online publication date: 15-Sep-2014
https://dl.acm.org/doi/10.1145/2629644
Farzan AKincaid ZPodelski A(2014)Proofs that countACM SIGPLAN Notices10.1145/2578855.253588549:1(151-164)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535885
Farzan AKincaid ZPodelski AJagannathan SSewell P(2014)Proofs that countProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2535838.2535885(151-164)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2535838.2535885
Esparza JLuttenberger MSchlund M(2014)A Brief History of Strahler NumbersProceedings of the 8th International Conference on Language and Automata Theory and Applications - Volume 837010.1007/978-3-319-04921-2_1(1-13)Online publication date: 10-Mar-2014
https://dl.acm.org/doi/10.1007/978-3-319-04921-2_1
Lin A(2012)Weakly-Synchronized ground tree rewritingProceedings of the 37th international conference on Mathematical Foundations of Computer Science10.1007/978-3-642-32589-2_55(630-642)Online publication date: 27-Aug-2012
https://dl.acm.org/doi/10.1007/978-3-642-32589-2_55
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents