@proceedings {BacciC10absdiag,
	title = {Abstract Diagnosis of First Order Functional Logic Programs},
	journal = {Logic-Based Program Synthesis and Transformation {\textendash} 20th International Symposium {\textendash} Pre-Proceedings},
	volume = {10-14},
	year = {2010},
	pages = {58{\textendash}72},
	edition = {20},
	address = {Hagenberg, Austria},
	abstract = {We present a generic scheme for the abstract debugging of functional-logic programs. We associate to our programs a semantics based on a (continuous) immediate consequence operator, P[[R]], which models correctly the typical cogent features of modern functional-logic languages (non-deterministic, non-strict functions defined by non-confluent programs and call-time choice behaviour). Then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness.},
	keywords = {Abstract Diagnosis, Debugging, Declarative Diagnosis, Functional-logic Programming},
	author = {Giovanni Bacci and Marco Comini},
	editor = {Maria Alpuente}
}
@proceedings {AlpuenteCEFL02,
	title = {Abstract Diagnosis of Functional Programs},
	journal = {Logic Based Program Synthesis and Tranformation {\textendash} 12th International Workshop, LOPSTR 2002, Revised Selected Papers},
	volume = {2664},
	year = {2003},
	publisher = {Springer-Verlag},
	address = {Berlin},
	abstract = {We present a generic scheme for the declarative debugging of functional programs modeled as (conditional) term rewriting systems. We associate to our programs a semantics based on a (continuous) immediate consequence operator, TR, which models the (values/normal forms) semantics of R. Then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness.

We have made available a prototypical implementation in Haskell and have tested it on some non trivial examples.},
	keywords = {Abstract Diagnosis, Abstract Interpretation, Abstract Verification, Declarative Debugging, Functional Programming, Inductive Verification},
	author = {Maria Alpuente and Marco Comini and Santiago Escobar and Moreno Falaschi and Salvador Lucas},
	editor = {Leuschel, M.}
}
@article {CominiGLV99,
	title = {Abstract Interpretation based Verification of Logic Programs},
	journal = {Science of Computer Programming},
	volume = {49},
	number = {1{\textendash}3},
	year = {2003},
	pages = {89{\textendash}123},
	abstract = {This paper is an overview of our results on the application of abstract interpretation concepts to various problems related to the verification of logic programs. These include the systematic design of semantics modeling various proof methods and the characterization of assertions as abstract domains.},
	keywords = {Abstract Diagnosis, Abstract Interpretation, Abstract Verification, Assertion Language, Inductive Verification, Logic Programming},
	author = {Marco Comini and Roberta Gori and Giorgio Levi and Volpe, P.}
}
@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 {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.}
}
