Giorgio Levi

I&C Journal 2003 Journal Article

Pair-independence and freeness analysis through linear refinement

• Giorgio Levi
• Fausto Spoto

Linear refinement is a technique for systematically constructing more precise abstract domains for program analysis starting from the basic domain which represents just the property of interest. We use here linear refinement to construct a domain for pair-independence and freeness analysis of logic programs which is strictly more precise than Jacobs and Langen’s domain for sharing analysis endowed with freeness information. Moreover, it can be used for abstract compilation, while Jacobs and Langen’s domain can only be used for abstract interpretation. We provide an approximate representation of our domain and algorithms for the abstract operations. We describe an implementation of an analyser which uses abstract compilation over our domain and its evaluation over a set of benchmarks. This shows that its precision is comparable to that of a traditional sharing and freeness analysis performed through abstract interpretation. To the best of our knowledge, this is the first implementation of a sharing analysis based on abstract compilation, as well as the first implementation of a static analysis based on a new domain developed through linear refinement.

I&C Journal 2001 Journal Article

A Theory of Observables for Logic Programs

• Marco Comini
• Giorgio Levi
• Maria Chiara Meo

We define a semantic framework to reason about properties of abstractions of SLD-derivations. The framework allows us to address problems such as the relation between the (top-down) operational semantics and the (bottom-up) denotational semantics, the existence of a denotation for a set of definite clauses and their properties (compositionality w. r. t. various syntactic operators, correctness, minimality, and precision). Using abstract interpretation techniques to model abstraction allows us to state very simple conditions on the observables which guarantee the validity of several general theorems.

LPAR Conference 2001 Conference Paper

How to Transform an Analyzer into a Verifier

• Marco Comini
• Roberta Gori
• Giorgio Levi

Abstract In this paper we push forward the idea of applying the abstract interpretation concepts to the problem of Verification of programs. We consider the theory of abstract Verification as proposed in [ 5 ] and we show how it is possible to transform static analyzers with some suitable properties to obtain automatic Verification tools based on suficient verification conditions. We prove that the approach is general and flexible by showing three difierent Verification tools based on difierent domains of types for functional, logic and CLP programming. The verifier for functional programs is obtained from a static analyzer which implements one of the polymorphic type domains introduced by Cousot [ 8 ]. The one for logic programs is obtained from a static analyzer on a type domain designed by Codish and Lagoon [ 3 ], while the verifier for CLP programs is obtained from the type analyzer described in [ 15 ].

TCS Journal 1996 Journal Article

Foreword

• Giorgio Levi
• Mario Rodriguez-Artalejo

TCS Journal 1995 Journal Article

Incremental constraint satisfaction for equational logic programming

• María Alpuente
• Moreno Falaschi
• Giorgio Levi

In this paper we are concerned with an instance of the Constraint Logic Programming (CLP) scheme specialized in solving equations with respect to a Horn equational theory E. The intended structure H E is given by the finest partition induced by E on the Herbrand universe H over a finite one sorted alphabet. This work deals with the description of an incremental constraint solver as the kernel of an operational semantics for the language CLP( H E ). The primary issues are: how to verify the solvability of constraints in the structure ( H E ) by using some sound and complete semantic unification procedure such as narrowing, how to simplify constraints in a computation sequence, how to achieve incrementality in the computation process and how to profit from finitely failed derivations as a heuristic for optimizing the algorithms.

LPAR Conference 1992 Conference Paper

A Two Steps Semantics for Logic Programs with Negation

• Maurizio Gabbrielli
• Giorgio Levi
• Daniele Turi

Abstract We analyze programs with negation by transforming them in order to infer constrained atoms which are regarded as basic semantic objects. Two steps are performed. Step I refers to the positive fragment of the program and unfolds all positive literals so that only atoms and conditional atoms remain. Step II refers to the stratified fragment and replaces defined negative literals with inequalities and equalities.

TCS Journal 1992 Journal Article

Unfolding and fixpoint semantics of concurrent constraint logic programs

• Maurizio Gabbrielli
• Giorgio Levi

We present a new semantics for a language in the family of concurrent constraint logic languages. The semantics can be based on a notion of clause unfolding, since the language is closed under this transformation. The unfolding semantics is obtained as a limit of an infinite unfolding process. Unfolding is also used to define an immediate consequences operator and, therefore, a fixpoint semantics in the typical logic programming style. The result of both the unfolding and the fixpoint semantics is a set of reactive behaviors, which are trees abstractly representing all the possible computations of a program, including deadlocks and finite failures.

TCS Journal 1991 Journal Article

Editorial

• Giorgio Levi

TCS Journal 1990 Journal Article

Finite failures and partial computations in concurrent logic languages

• Moreno Falaschi
• Giorgio Levi

This paper investigates some semantic properties of concurrent logic languages. Concurrent logic languages with a commit operator differ from pure logic languages in the finite failure set. Since the new finite failure set depends on the computation rule, we define an operational semantics based on a parallel computation rule and a fair search rule. Failures with a parallel computation rule are shown to be strongly related to partial computed answer substitutions. The set of partial computed answer substitutions and the set of finite failures are defined as the least fixpoint of a transformation on pairs of interpretations.

TCS Journal 1988 Journal Article

Editorial

• Giorgio Levi
• Ugo Montanari

AIJ Journal 1976 Journal Article

Generalized and/or graphs

• Giorgio Levi
• Franco Sirovich

A generalization of AND/OR graphs is introduced as a problem solving model, in which subproblem interdependence in problem reduction can be explicitly accounted for. An ordered-search algorithm is given to find a solution. The algorithm is proven to be admissible and optimal. Examples are given which show the application of the formalism to problems which cannot be modelled by AND/OR graphs. Generalized AND/OR graphs are finally shown to be equivalent to type O grammars. Finding a solution of a generalized AND/OR graph is shown to be equivalent to deriving a sentence in the corresponding type O grammar.

MFCS Conference 1975 Conference Paper

Proving Program Properties, Symbolic Evaluation and Logical Procedural Semantics

• Giorgio Levi
• Franco Sirovich