More Web Proxy on the site http://driver.im/

Article

Abstract Interpretation of Indexed Grammars

Authors:

Mila Dalla Preda,

Roberto GiacobazziAuthors Info & Claims

Static Analysis: 26th International Symposium, SAS 2019, Porto, Portugal, October 8–11, 2019, Proceedings

Pages 121 - 139

https://doi.org/10.1007/978-3-030-32304-2_7

Published: 08 October 2019 Publication History

Abstract

Indexed grammars are a generalization of context-free grammars and recognize a proper subset of context-sensitive languages. The class of languages recognized by indexed grammars are called indexed languages and they correspond to the languages recognized by nested stack automata. For example indexed grammars can recognize the language [inline-graphic not available: see fulltext] which is not context-free, but they cannot recognize [inline-graphic not available: see fulltext] which is context-sensitive. Indexed grammars identify a set of languages that are more expressive than context-free languages, while having decidability results that lie in between the ones of context-free and context-sensitive languages. In this work we study indexed grammars in order to formalize the relation between indexed languages and the other classes of languages in the Chomsky hierarchy. To this end, we provide a fixpoint characterization of the languages recognized by an indexed grammar and we study possible ways to abstract, in the abstract interpretation sense, these languages and their grammars into context-free and regular languages.

References

[1]

Adams J, Freden E, and Mishna M From indexed grammars to generating functions RAIRO Theor. Inform. Appl. 2013 47 4 325-350

[2]

Aho AV Indexed grammars - an extension of context-free grammars J. ACM 1968 15 4 647-671

[3]

Aho AV Nested stack automata J. ACM 1969 16 3 383-406

[4]

Ballance, R.A., Butcher, J., Graham, S.L.: Grammatical abstraction and incremental syntax analysis in a language-based editor. In: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, PLDI 1988, pp. 185–198. ACM, New York (1988)

[5]

Bertsch E On the relationship between indexed grammars and logic programs J. Log. Program. 1994 18 1 81-98

[6]

Chomsky N On certain formal properties of grammars Inf. Control. 1959 2 2 137-167

[7]

Clarke EM, Grumberg O, and Jha S Verifying parameterized networks ACM Trans. Program. Lang. Syst. 1997 19 5 726-750

[8]

Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational System Design, vol. 173, pp. 421–505. NATO Science Series, Series F: Computer and Systems Sciences. IOS Press, Amsterdam (1999)

[9]

Cousot P Constructive design of a hierarchy of semantics of a transition system by abstract interpretation Theor. Comput. Sci. 2002 277 1–2 47-103

[10]

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL 1977), pp. 238–252. ACM Press (1977)

[11]

Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the 6th ACM Symposium on Principles of Programming Languages (POPL 1979), pp. 269–282. ACM Press (1979)

[12]

Cousot P and Cousot R Abstract interpretation frameworks J. Log. Comput. 1992 2 4 511-547

[13]

Cousot P and Cousot R Wolper P Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form (Invited Paper) Computer Aided Verification 1995 Heidelberg Springer 293-308

[14]

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 84–96. ACM Press (1978)

[15]

Cousot P and Cousot R Grammar semantics, analysis and parsing by abstract interpretation Theor. Comput. Sci. 2011 412 44 6135-6192

[16]

Cousot, P., Cousot, R.: Abstract interpretation: past, present and future. In: Henzinger, T.A., Miller, D. (eds.) Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, Vienna, Austria, 14–18 July 2014, pp. 2:1–2:10. ACM (2014)

[17]

Dalla Preda M, Giacobazzi R, Debray S, Coogan K, and Townsend GM Cousot R and Martel M Modelling metamorphism by abstract interpretation Static Analysis 2010 Heidelberg Springer 218-235

[18]

Dalla Preda M, Giacobazzi R, and Debray SK Unveiling metamorphism by abstract interpretation of code properties Theor. Comput. Sci. 2015 577 74-97

[19]

Deutsch A Interprocedural may-alias analysis for pointers: beyond k-limiting SIGPLAN Not. 1994 29 6 230-241

[20]

Gazdar G Reyle U and Rohrer C Applicability of indexed grammars to natural languages Natural Language Parsing and Linguistic Theories 1988 Dordrecht Springer 69-94

[21]

Giacobazzi R, Ranzato F, and Scozzari F Making abstract interpretation complete J. ACM. 2000 47 2 361-416

[22]

Ginsburg S The Mathematical Theory of Context Free Languages 1966 New York McGraw-Hill Book Company

[23]

Istrail S Generalization of the Ginsburg-Rice Schützenberger fixed-point theorem for context-sensitive and recursive-enumerable languages Theor. Comput. Sci. 1982 18 3 333-341

[24]

Partee BB, ter Meulen AG, and Wall R Mathematical Methods in Linguistics 2012 Dordrecht Springer

Cited By

Ciobanu LZetzsche GSobocinski PLago UEsparza J(2024)Slice closures of indexed languages and word equations with counting constraintsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662134(1-12)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662134
Campion MUrban CDalla Preda MGiacobazzi R(2023)A Formal Framework to Measure the Incompleteness of Abstract InterpretationsStatic Analysis10.1007/978-3-031-44245-2_7(114-138)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44245-2_7
Campion MDalla Preda MGiacobazzi R(2022)Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysisProceedings of the ACM on Programming Languages10.1145/34987216:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498721

Index Terms

Abstract Interpretation of Indexed Grammars
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation
  1. Formal languages and automata theory
    1. Formalisms
      1. Rewrite systems
    2. Grammars and context-free languages
  2. Semantics and reasoning
    1. Program semantics

Index terms have been assigned to the content through auto-classification.

Recommendations

Sequentially Indexed Grammars

This article defines the grammar class of sequentially indexed grammars (SIGs) that results of a change in the index stack handling mechanism of indexed grammars (Aho, 1968, Journal of the ACM, 15, 647–671; 1969, Journal of the ACM, 16, 383–406). SIGs ...
Indexed Grammars—An Extension of Context-Free Grammars

A new type of grammar for generating formal languages, called an indexed grammar, is presented. An indexed grammar is an extension of a context-free grammar, and the class of languages generated by indexed grammars has closure properties and ...
Parsers for indexed grammars

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Static Analysis: 26th International Symposium, SAS 2019, Porto, Portugal, October 8–11, 2019, Proceedings

Oct 2019

483 pages

ISBN:978-3-030-32303-5

DOI:10.1007/978-3-030-32304-2

Editor:
Bor-Yuh Evan Chang
University of Colorado, Boulder, CO, USA

© Springer Nature Switzerland AG 2019.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 08 October 2019

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 18 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ciobanu LZetzsche GSobocinski PLago UEsparza J(2024)Slice closures of indexed languages and word equations with counting constraintsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662134(1-12)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662134
Campion MUrban CDalla Preda MGiacobazzi R(2023)A Formal Framework to Measure the Incompleteness of Abstract InterpretationsStatic Analysis10.1007/978-3-031-44245-2_7(114-138)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44245-2_7
Campion MDalla Preda MGiacobazzi R(2022)Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysisProceedings of the ACM on Programming Languages10.1145/34987216:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498721

View Options

View options

Media

Figures

Other

Tables

View Table of Contents