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

2001 ◽  
pp. 243-261 ◽  
Author(s):  
John P. Gallagher ◽  
Germán Puebla
Keyword(s):  
Abstract Interpretation ◽  
Tree Automata ◽  
Logic Programs ◽  
Finite Tree

Deciding Equivalence of Finite Tree Automata

1990 ◽  
Vol 19 (3) ◽  
pp. 424-437 ◽  
Author(s):  
Helmut Seidl
Keyword(s):  
Tree Automata ◽  
Finite Tree

scholarly journals Bottom-up abstract interpretation of logic programs

1994 ◽  
Vol 124 (1) ◽  
pp. 93-125 ◽  
Author(s):  
Michael Codish ◽  
Dennis Dams ◽  
Eyal Yardeni
Keyword(s):  
Abstract Interpretation ◽  
Logic Programs ◽  
Bottom Up

Improving Execution Models of Logic Programs by Two-phase Abstract Interpretation

ETRI Journal ◽  
1995 ◽  
Vol 16 (4) ◽  
pp. 27-47
Author(s):  
Byeong-Mo Chang Chang ◽  
Kwang-Moo Choe Choe ◽  
Roberto Giacobazzi Giacobazzi
Keyword(s):  
Abstract Interpretation ◽  
Logic Programs ◽  
Two Phase ◽  
Execution Models

scholarly journals A backward analysis for constraint logic programs

2002 ◽  
Vol 2 (4-5) ◽  
pp. 517-547 ◽  
Author(s):  
ANDY KING ◽  
LUNJIN LU
Keyword(s):  
Ad Hoc ◽  
Abstract Interpretation ◽  
Logic Program ◽  
Control Flow ◽  
Third Party ◽  
Logic Programs ◽  
Abstract Domains ◽  
Constraint Logic Programs ◽  
Backward Analysis ◽  
Computational Properties

One recurring problem in program development is that of understanding how to re-use code developed by a third party. In the context of (constraint) logic programming, part of this problem reduces to figuring out how to query a program. If the logic program does not come with any documentation, then the programmer is forced to either experiment with queries in an ad hoc fashion or trace the control-flow of the program (backward) to infer the modes in which a predicate must be called so as to avoid an instantiation error. This paper presents an abstract interpretation scheme that automates the latter technique. The analysis presented in this paper can infer moding properties which if satisfied by the initial query, come with the guarantee that the program and query can never generate any moding or instantiation errors. Other applications of the analysis are discussed. The paper explains how abstract domains with certain computational properties (they condense) can be used to trace control-flow backward (right-to-left) to infer useful properties of initial queries. A correctness argument is presented and an implementation is reported.

scholarly journals Abstract interpretation and application to logic programs

1992 ◽  
Vol 13 (2-3) ◽  
pp. 103-179 ◽  
Author(s):  
Patrick Cousot ◽  
Radhia Cousot
Keyword(s):  
Abstract Interpretation ◽  
Logic Programs

scholarly journals Optimality in goal-dependent analysis of Sharing

2009 ◽  
Vol 9 (05) ◽  
pp. 617-689 ◽  
Author(s):  
GIANLUCA AMATO ◽  
FRANCESCA SCOZZARI
Keyword(s):  
Logic Programming ◽  
Static Analysis ◽  
Abstract Interpretation ◽  
Logic Programs ◽  
Semantic Operators

AbstractWe face the problems of correctness, optimality, and precision for the static analysis of logic programs, using the theory of abstract interpretation. We propose a framework with a denotational, goal-dependent semantics equipped with two unification operators for forward unification (calling a procedure) and backward unification (returning from a procedure). The latter is implemented through a matching operation. Our proposal clarifies and unifies many different frameworks and ideas on static analysis of logic programming in a single, formal setting. On the abstract side, we focus on the domainsharingby Jacobs and Langen (The Journal of Logic Programming, 1992, vol. 13, nos. 2–3, pp. 291–314) and provide the best correct approximation of all the primitive semantic operators, namely, projection, renaming, and forward and backward unifications. We show that the abstract unification operators are strictly more precise than those in the literature defined over the same abstract domain. In some cases, our operators are more precise than those developed for more complex domains involving linearity and freeness.

Sign in / Sign up

Export Citation Format

Share Document