We show how to transform a set of regular type definitions into a finite pre-interpretation for a logic program. The derived preinterpretation forms the basis for an abstract interpretation. The core of the transformation is a determinization procedure for non-deterministic finite tree automata. This approach provides a flexible and practical way of building program-specific analysis domains. We argue that the constructed domains are condensing: thus goal-independent analysis over the constructed domains loses no precision compared to goal-dependent analysis. We also show how instantiation modes such as ground, variable and non-variable can be expressed as regular types and hence integrated with other regular types. We highlight applications in binding time analysis for offline partial evaluation and infinite-state model checking. Experimental results and a discussion of complexity are included. © Springer-Verlag 2004.
CITATION STYLE
Gallagher, J. P., & Henriksen, K. S. (2004). Abstract domains based on regular types. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3132, 27–42. https://doi.org/10.1007/978-3-540-27775-0_3
Mendeley helps you to discover research relevant for your work.