1,720,969 research outputs found
An Abstract Interpretation Framework which Accurately Handles Prolog Search-Rule and the Cut
No full text
Sequence-based Abstract Interpretation of Prolog
No full textMany abstract interpretation frameworks and analyses for Prolog have been proposed, which seek to extract information useful for program optimization. Although motivated by practical considerations, notably making Prolog competitive with imperative languages, such frameworks fail to capture some of the control structures of existing implementations of the language.
In this paper we propose a novel framework for the abstract interpretation of Prolog which handles the depth-first search rule and the cut operator. It relies on the notion of substitution sequence to model the result of the execution of a goal. The framework consists of (i) a denotational concrete semantics, (ii) a safe abstraction of the concrete semantics defined in terms of a class of post-fixpoints, and (iii) a generic abstract interpretation algorithm. We show that traditional abstract domains of substitutions may easily be adapted to the new framework, and provide experimental evidence of the effectiveness of our approach. We also show that previous work on determinacy analysis, that was not expressible by existing abstract interpretation frameworks, can be seen as an instance of our framework
Reexecution-Based Analysis of Logic Programs with Delay Declarations.
Full text linkA general semantics-based framework for the analysis of logic programs with delay declarations is presented. The framework incorporates well known refinement techniques based on reexecution. The concrete and abstract semantics express both deadlock information and qualified answers
Automated Verification of Prolog Programs
No full textAlthough Prolog is (still) the most widely used logic language, it suffers from a number of drawbacks which prevent it from being truely declarative. The nondeclarative features such as the depth-first search rule are nevertheless necessary to make Prolog reasonably efficient. Several authors have proposed methodologies to reconcile declarative programming with the algorithmic features of Prolog. The idea is to analyse the logic program with respect to a set of properties such as modes, types, sharing, termination, and the like in order to ensure that the operational behaviour of the Prolog program complies with its logic meaning. Such analyses are tedious to perform by hand and can be automated to some extent. This paper presents a state-of-the-art analyser which allows one to integrate many individual analyses previously proposed in the literature as well as new ones. Conceptually, the analyser is based on the notion of abstract sequence which makes it possible to collect all kinds of desirable information, including relations between the input and output sizes of terms, multiplicity, and termination
Distinctness and Sharing Domains for Static Analysis of Java Programs
Full text linkThe applicatio fieldo f static analysis techniques foo b ectot -j ted proD81 ming is getting bro9 er, rangingfro co pilero ptimizatio s to security issues. This leadsto the needo metho do`D000 that suppoD reusability n o o ly at the co de level butalso at higher (semantic) levels, ino rderto minimize the e#o rto fpro ving co rrectness o the analyses. Abstract interpretatio may be the mo st appr o riate appro ach in that respect. This paper is a co ntributio n to wards the designo f a general framewoj fo abstract interpretatio o Java pro92D s. We intro duce two generic abstract do mains that express type, structural, and sharing infoD atio ab o t dynamically createdo b ects. These generic do mains can be instantiated to get specific analyses either foo ptimizatio no r verificatio n issues. The semanticso f thedo mains are precisely defined by meanso f co ncretizatio n functio ns basedo n mappings between co ncrete and abstract lo catio ns. The main abstracto peratio ns, i.e., upper bo und and assignment, are discussed. An applicatio no f thedo mains to so rce-t oso rce proD0D specializatio is sketched to illustrate the e#ectiveness o the analysis
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
EVALUATION OF THE DOMAIN PROP
No full textThe domain Prop [11, 30] is a conceptually simple and elegant abstract do-main to compute groundness information for Prolog programs, where ab-stract substitutions are represented by Boolean functions. Prop has raised much theoretical interest recently, but little is known about the practical accuracy and efficiency of this domain. Experimental evaluation of Prop is particularly important since Prop theoretically needs to solve a co-NP-Complete problem. However, this complexity issue may not matter much in practice because the size of the abstract substitutions is bounded since Prop would only work on the clause variables in many frameworks. The purpose of this paper is to study the performance of domain Prop. Its first contribution is to describe an implementation of the domain Prop and to use it to instantiate a generic abstract interpretation algorithm [17, 23, 27]. A key feature of the implementation is the use of ordered binary decision graphs to provide a compact representation of many Boolean functions. Its second contribution is to describe the design and implementation of a new domain, Pat (Prop), combining the domain Prop with structural infor-mation about the subterms. This new domain may significantly improve the accuracy of the domain Prop on programs manipulating difference-lists. Both implementations (resp. 6000 and 12,000 lines of C) have been evaluated systematically, and their efficiency and accuracy for groundness inference have been compared with several other abstract domains. The interest of Pat (Prop) and Prop for on-line analysis is also investigated
- …
