@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.}
}
@proceedings {Comini02,
	title = {VeriPolyTypes: a tool for Verification of Logic Programs with respect to Type Specifications},
	journal = {Proceedings of 11th International Workshop on Functional and (constraint) Logic Programming},
	number = {UDMI/18/2002/RR},
	year = {2002},
	pages = {233{\textendash}236},
	publisher = {Dipartimento di Matematica e Informatica, Universit{\`a} di Udine},
	address = {Udine, Italy},
	abstract = {In this system demonstration we present a tool for the verification of Logic Programs w.r.t. type information specifications. The tool is based on sufficient verification conditions obtained by abstract interpretation.

Following the theoretical foundation in [CominiGL01,CominiGLV99entcs,CominiGLV99], the tool is obtained by transforming a static analyzer on a type domain for Logic Programs designed by Codish and Lagoon [CodishL98].},
	keywords = {Abstract Interpretation, Abstract Verification, Inductive Verification, Logic Programming},
	author = {Marco Comini},
	editor = {Moreno Falaschi}
}
@proceedings {CominiGL01,
	title = {How to Transform an Analyzer into a Verifier},
	journal = {Logic for Programming and Automated Reasoning. Proceedings of the 8th International Conference (LPAR{\textquoteright}01)},
	volume = {2250},
	year = {2001},
	pages = {595{\textendash}609},
	publisher = {Springer-Verlag},
	address = {Berlin},
	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 [CominiGLV99entcs,CominiGLV99] and we show how it is possible to transform static analyzers with some suitable properties to obtain automatic verification tools based on sufficient verification conditions. We prove that the approach is general and flexible by showing three different verification tools based on different domains of types for functional, logic programming 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 [Cousot97c]. The one for logic programs is obtained from a static analyzer on a type domain designed by Codish and Lagoon [CodishL98], while the verifier for CLP programs is obtained starting from the type analyzer described in [DrabentP98].},
	keywords = {Abstract Interpretation, Abstract Verification, Inductive Verification},
	author = {Marco Comini and Roberta Gori and Giorgio Levi},
	editor = {Nieuwenhuis, R. and Voronkov, A.}
}
