TY - GEN
T1 - Abstract interpretation over non-deterministic finite tree automata for set-based analysis of logic programs
AU - Gallagher, John P.
AU - Puebla, Germán
PY - 2002
Y1 - 2002
N2 - 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.
AB - 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.
U2 - 10.1007/3-540-45587-6_16
DO - 10.1007/3-540-45587-6_16
M3 - Article in proceedings
AN - SCOPUS:84947241479
SN - 354043092X
SN - 9783540430926
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 243
EP - 261
BT - Practical Aspects of Declarative Languages
A2 - Krishnamurthi, Shriram
A2 - Ramakrishnan, C.R.
PB - Springer Verlag
T2 - 4th International Symposium on Practical Applications of Declarative Languages, PADL 2002
Y2 - 19 January 2002 through 20 January 2002
ER -