×

zbMATH — the first resource for mathematics

String analysis as an abstract interpretation. (English) Zbl 1317.68099
Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 294-308 (2011).
Summary: We formalize a string analysis within abstract interpretation framework. The abstraction of strings is given as a conjunction of predicates that describes the common configuration changes on the reference pushdown automaton while processing the strings. We also present a family of pushdown automata called \(\epsilon \) bounded pushdown automata. This family covers all context-free languages, and by using this family of pushdown automata, we can prevent abstract values from becoming infinite conjunctions and guarantee that the operations required in the analyzer are computable.
For the entire collection see [Zbl 1206.68013].
MSC:
68Q45 Formal languages and automata
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC 2004: Proceedings of the Thirty-Sixth Annual ACM Symposium on Theory of Computing, pp. 202–211. ACM, New York (2004) · Zbl 1192.68396 · doi:10.1145/1007352.1007390
[2] Bates, J., Lavie, A.: Recognizing substrings of LR(k) languages in linear time. ACM Trans. Program. Lang. Syst. 16(3), 1051–1077 (1994) · doi:10.1145/177492.177768
[3] Billot, S., Lang, B.: The structure of shared forests in ambiguous parsing. In: Proceedings of the 27th Annual Meeting on Association for Computational Linguistics, pp. 143–151. Association for Computational Linguistics, Morristown (1989) · doi:10.3115/981623.981641
[4] Choi, T.-H., Lee, O., Kim, H., Doh, K.-G.: A practical string analyzer by the widening approach. In: APLAS, pp. 374–388 (2006) · Zbl 1168.68359 · doi:10.1007/11924661_23
[5] Christensen, A.S., Møller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1–18. Springer, Heidelberg (2003), http://www.brics.dk/JSA/ · Zbl 1067.68541 · doi:10.1007/3-540-44898-5_1
[6] Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992) · Zbl 0783.68073 · doi:10.1093/logcom/2.4.511
[7] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM, New York (1977)
[8] Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 269–282. ACM, New York (1979) · Zbl 1323.68356
[9] Doh, K.-G., Kim, H., Schmidt, D.A.: Abstract parsing: Static analysis of dynamically generated string output using LR-parsing technology. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 256–272. Springer, Heidelberg (2009) · Zbl 05596310 · doi:10.1007/978-3-642-03237-0_18
[10] Friedman, E.P.: The inclusion problem for simple languages. Theor. Comput. Sci. 1(4), 297–316 (1976) · Zbl 0349.68032 · doi:10.1016/0304-3975(76)90074-8
[11] Goeman, H.: On parsing and condensing substrings of LR languages in linear time. Theor. Comput. Sci. 267(1-2), 61–82 (2001) · Zbl 0984.68093 · doi:10.1016/S0304-3975(00)00296-6
[12] Greibach, S.A., Friedman, E.P.: Superdeterministic pdas: A subcase with a decidable inclusion problem. J. ACM 27(4), 675–700 (1980) · Zbl 0462.68030 · doi:10.1145/322217.322224
[13] Greibach, S.A.: A new normal-form theorem for context-free phrase structure grammars. J. ACM 12(1), 42–52 (1965) · Zbl 0135.18404 · doi:10.1145/321250.321254
[14] Kim, S.-W.: Proofs for formalizing string analysis within abstract interpretation framework. Technical report, KAIST (2010), http://pllab.kaist.ac.kr/ sewon.kim/papers/pf-saai-tr.pdf
[15] Kirkegaard, C., Møller, A.: Static analysis for java servlets and JSP. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 336–352. Springer, Heidelberg (2006) · Zbl 05528263 · doi:10.1007/11823230_22
[16] Knuth, D.E.: A characterization of parenthesis languages. Information and Control 11(3), 269–289 (1967) · Zbl 0196.01703 · doi:10.1016/S0019-9958(67)90564-5
[17] Kong, S., Choi, W., Yi, K.: Abstract parsing for two-staged languages with concatenation. In: GPCE 2009: Proceedings of the Eighth International Conference on Generative Programming and Component Engineering, pp. 109–116. ACM, New York (2009) · doi:10.1145/1621607.1621625
[18] Lang, B.: Deterministic techniques for efficient non-deterministic parsers. In: Loeckx, J. (ed.) ICALP 1974. LNCS, vol. 14, pp. 255–269. Springer, Heidelberg (1974) · Zbl 0299.68020 · doi:10.1007/3-540-06841-4_65
[19] Lang, B.: Parsing incomplete sentences. In: Proceedings of the 12th conference on Computational linguistics, pp. 365–371. ACL, Morristown (1988) · doi:10.3115/991635.991710
[20] Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005) · Zbl 1108.68427 · doi:10.1007/978-3-540-31987-0_2
[21] Minamide, Y.: Static approximation of dynamically generated web pages. In: WWW 2005: Proceedings of the 14th International Conference on World Wide Web, pp. 432–441. ACM, New York (2005)
[22] Minamide, Y., Tozawa, A.: Xml validation for context-free grammars. In: APLAS, pp. 357–373 (2006) · Zbl 1168.68362 · doi:10.1007/11924661_22
[23] Nederhof, M.-J., Bertsch, E.: Linear-time suffix parsing for deterministic languages. J. ACM 43(3), 524–554 (1996) · Zbl 0882.68022 · doi:10.1145/233551.233555
[24] Vallée-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot - a java optimization framework. In: Proceedings of CASCON 1999, pp. 125–135 (1999)
[25] Rekers, J., Koorn, W.: Substring parsing for arbitrary context-free grammars. SIGPLAN Not. 26(5), 59–66 (1991) · doi:10.1145/122501.122505
[26] Thiemann, P.: Grammar-based analysis of string expressions. In: TLDI 2005: Proceedings of the 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 59–70. ACM, New York (2005) · doi:10.1145/1040294.1040300
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.