@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.}
}
@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.}
}
@proceedings {CominiLV95a,
	title = {Declarative Diagnosis Revisited},
	journal = {Proceedings of the 1995 Int{\textquoteright}l Symposium on Logic Programming},
	year = {1995},
	pages = {275{\textendash}287},
	publisher = {The MIT Press},
	abstract = {We extend the declarative diagnosis methods to the diagnosis w.r.t. computed answers. We show that absence of uncovered atoms implies completeness for a large class of programs. We then define a top-down diagnoser, which uses one oracle only, does not require to determine in advance the symptoms and is driven by a (finite) set of goals. Finally we tackle the problem of effectivity, by introducing (finite) partial specifications. We obtain an effective diagnosis method, which is weaker than the general one in the case of correctness, yet can efficiently be implemented in both a top-down and in a bottom-up style.},
	author = {Marco Comini and Giorgio Levi and Vitiello, G.},
	editor = {Lloyd, J.}
}
@proceedings {CominiLV95,
	title = {Efficient Detection of Incompleteness Errors in the Abstract Debugging of Logic Programs},
	journal = {Proc. 2nd International Workshop on Automated and Algorithmic Debugging, AADEBUG{\textquoteright}95},
	year = {1995},
	abstract = {Abstract debugging of logic programs is an extension of declarative debugging, where we deal with specifications of operational properties, which can be characterized as abstractions of SLD-trees (observables).
We introduce a simple and efficient method to detect incompleteness errors, which is based on the application of the immediate consequences operator to the specification. The method is proved to be correct and complete whenever the immediate consequences operator has a unique fixpoint. We then prove that this property is always satisfied if the program belongs to a large class of programs (acceptable programs). We finally show that the same property can be proved for any program P, if the observable belongs to a suitable class of observables.},
	author = {Marco Comini and Giorgio Levi and Vitiello, G.},
	editor = {Ducass{\'e}, M.}
}
@proceedings {CominiLV94,
	title = {Abstract Debugging of Logic Programs},
	journal = {Proc. Logic Program Synthesis and Transformation and Metaprogramming in Logic 1994},
	volume = {883},
	year = {1994},
	pages = {440{\textendash}450},
	publisher = {Springer-Verlag},
	abstract = {Abstract debugging of logic programs is a novel combination of three known techniques, i.e. algorithmic (declarative) debugging, the s-semantics approach to the definition of program denotations modeling various observable behaviors, and abstract interpretation.},
	author = {Marco Comini and Giorgio Levi and Vitiello, G.},
	editor = {Fribourg, L. and Turini, F.}
}
