@article {CominiLM96,
	title = {A Theory of Observables for Logic Programs},
	journal = {Information and Computation},
	volume = {169},
	year = {2001},
	pages = {23{\textendash}80},
	publisher = {Academic Press},
	address = {New York},
	abstract = {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.},
	keywords = {Abstract Interpretation, Compositionality, Logic Programming, Semantics, SLD-derivations},
	author = {Marco Comini and Giorgio Levi and Maria Chiara Meo}
}
@article {CominiLMV96a,
	title = {Abstract Diagnosis},
	journal = {Journal of Logic Programming},
	volume = {39},
	number = {1-3},
	year = {1999},
	pages = {43{\textendash}93},
	abstract = {We show how declarative diagnosis techniques can be extended to cope with verification of operational properties, such as computed and correct answers, and of abstract properties, such as depth(k) answers and groundness dependencies. The extension is achieved by using a simple semantic framework, based on abstract interpretation. The resulting technique (abstract diagnosis) leads to elegant bottom-up and top-down verification methods, which do not require to determine the symptoms in advance, and which are effective in the case of abstract properties described by finite domains.},
	keywords = {Debugging, Declarative Diagnosis, Logic Programming, Semantics, Verification},
	author = {Marco Comini and Giorgio Levi and Maria Chiara Meo and Vitiello, G.}
}
@mastersthesis {Comini98,
	title = {An Abstract Interpretation Framework for Semantics and Diagnosis of Logic Programs},
	number = {5/98},
	year = {1998},
	pages = {1{\textendash}307},
	school = {Dipartimento di Informatica, Universit{\'a} di Pisa},
	type = {phd},
	address = {Pisa, Italy},
	abstract = {We define a semantic framework to reason about properties of abstractions of SLD-derivations (observables). The framework allows us to address problems such as the relation between the operational semantics and the denotational semantics and their properties (compositionality w.r.t. various syntactic operators, correctness and minimality, precision degree). Using abstract interpretation techniques to model abstraction allows us to state algebraic conditions on the observables which guarantee the validity of several compositionality and equivalence theorems.
We then use the semantic framework to extend declarative debugging techniques to cope with the analysis of operational properties, such as computed and correct answers, and of abstract properties, such as depth(k) answers and groundness dependencies. The resulting technique (abstract diagnosis) leads to elegant bottom-up and top-down diagnosis methods, which do not require to determine the symptoms in advance, and which are effective in the case of abstract properties described by finite domains.},
	keywords = {Abstract Diagnosis, Abstract Interpretation, Compositionality, Declarative Debugging, Inductive Verification, Logic Programming, Semantics, SLD-derivations},
	author = {Marco Comini}
}
@proceedings {CominiLV97,
	title = {Modular Abstract Diagnosis},
	journal = {Proceedings APPIA-GULP-PRODE{\textquoteright}98 Joint Conference on Declarative Programming},
	year = {1998},
	pages = {409{\textendash}420},
	abstract = {The paper extends the Abstract Diagnosis framework to Modular Abstract Diagnosis, where we are concerned with programs composed of separate modules. Our theory of abstract diagnosis can be applied to modular diagnosis even if our concrete semantics is not OR-compositional. Abstract diagnosis is a generalization of declarative diagnosis, where we consider operational properties, i.e. observables, which are properties which can be extracted from a goal computation.},
	keywords = {Debugging, Declarative Diagnosis, Logic Programming, Semantics, Verification},
	author = {Marco Comini and Giorgio Levi and Vitiello, G.},
	editor = {Freire-Nistal, J. L. and Moreno Falaschi and Villares-Ferro, M.}
}
@proceedings {CominiLMV96,
	title = {Proving properties of Logic Programs by Abstract Diagnosis},
	journal = {Proceedings of Analysis and Verification of Multiple-Agent Languages, 5th LOMAPS Workshop (LOMAPS{\textquoteright}96)},
	volume = {1192},
	year = {1996},
	pages = {22{\textendash}50},
	publisher = {Springer-Verlag},
	address = {Berlin},
	abstract = {We show how declarative diagnosis techniques can be extended to cope with verification of operational properties, such as computed answers, and of abstract properties, such as types and groundness dependencies. The extension is achieved by using a simple semantic framework, based on abstract interpretation. The resulting technique (abstract diagnosis) leads to elegant bottom-up and top-down verification methods, which do not require to determine the symptoms in advance, and which are effective in the case of abstract properties described by finite domains.},
	keywords = {Abstract Diagnosis, Abstract Interpretation, Declarative Debugging, Inductive Verification, Logic Programming, Semantics},
	author = {Marco Comini and Giorgio Levi and Maria Chiara Meo and Vitiello, G.},
	editor = {Dams, M.}
}
