Abstract Interpretation over Non-deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs

JP Gallagher, G Puebla

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

32 Citations (Scopus)

Abstract

Set-based program analysis has many potential applications, including compiler optimisations, type-checking, debugging, verification and planning. One method of set-based analysis is to solve a set of set constraints derived directly from the program text. Another approach is based on abstract interpretation (with widening) over an infinite-height domain of regular types. Up till now only deterministic types have been used in abstract interpretations, whereas solving set constraints yields non-deterministic types, which are more precise. It was pointed out by Cousot and Cousot that set constraint analysis of a particular program P could be understood as an abstract interpretation over a finite domain of regular tree grammars, constructed from P. In this paper we define such an abstract interpretation for logic programs, formulated over a domain of non-deterministic finite tree automata, and describe its implementation. Both goal-dependent and goal-independent analysis are considered. Variations on the abstract domains operations are introduced, and we discuss the associated tradeoffs of precision and complexity. The experimental results indicate that this approach is a practical way of achieving the precision of set-constraints in the abstract interpretation framework.
Translated title of the contributionAbstract Interpretation over Non-deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs
Original languageEnglish
Title of host publicationUnknown
EditorsShriram Krishnamurthi, C. R. Ramakrishnan
PublisherSpringer Berlin Heidelberg
Pages243 - 261
Number of pages18
ISBN (Print)354043092X
Publication statusPublished - Jan 2002

Bibliographical note

Conference Proceedings/Title of Journal: Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, LNCS Vol. 2257

Fingerprint Dive into the research topics of 'Abstract Interpretation over Non-deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs'. Together they form a unique fingerprint.

  • Cite this

    Gallagher, JP., & Puebla, G. (2002). Abstract Interpretation over Non-deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs. In S. Krishnamurthi, & C. R. Ramakrishnan (Eds.), Unknown (pp. 243 - 261). Springer Berlin Heidelberg. http://www.cs.bris.ac.uk/Publications/pub_info.jsp?id=1000612