@proceedings {BacciCFV12,
	title = {The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages},
	journal = {Technical Communications of the 28th International Conference on Logic Programming (ICLP 2012)},
	volume = {17},
	year = {2012},
	pages = {144-153},
	address = {Budapest, Hungary},
	abstract = {This paper discusses on the additional issues for the automatic inference of algebraic property-oriented specifications which arises because of interaction between laziness and logical variables in lazy functional logic languages.
We present an inference technique that overcomes these issues for the first-order fragment of the lazy functional logic language Curry. Our technique statically infers from the source code of a Curry program a specification which consists of a set of equations relating (nested) operation calls
that have the same behavior. Our proposal is a (glass-box) semantics-based inference method which can guarantee, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.},
	keywords = {Curry, property-oriented specifications, semantics-based inference methods},
	isbn = {978-3-939897-43-9},
	issn = {978-3-939897-43-9},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva},
	editor = {Agostino Dovier and V. Santos Costa}
}
@proceedings {CominiDV07,
	title = {On Polymorphic Recursion, Type Systems, and Abstract Interpretation},
	journal = {Static Analysis {\textendash} 15th International Symposium, SAS 2008},
	volume = {5079},
	year = {2008},
	pages = {144{\textendash}158},
	publisher = {Springer-Verlag},
	address = {Berlin},
	abstract = {The problem of typing polymorphic recursion (i.e. recursive function definitions rec{x = e} where different occurrences of x in e are used with different types) has been investigated both by people working on type systems and by people working on abstract interpretation.

Recently, Gori and Levi have developed an abstract interpreter that is able to type all the ML typable recursive definitions and interesting examples of polymorphic recursion. The problem of finding a type system corresponding to their abstract interpreter was open.

In this paper we present a type system corresponding to the Gori-Levi abstract interpreter. Interestingly enough, the type system is derived from the system of simple types (which is the let-free fragment of the ML type system) by adapting a general technique for extending a decidable type system enjoying principal typings by adding a decidable rule for typing recursive definitions. The key role played in our investigation by the notion of principal typing suggests that this notion might be useful in other investigations about the relations between type systems and type inference algorithms synthesized by abstract interpretation.},
	author = {Marco Comini and Ferruccio Damiani and Samuel Vrech},
	editor = {Maria Alpuente and Germ{\'a}n Vidal}
}
@proceedings {CominiGL00a,
	title = {Logic programs as specifications in the inductive verification of logic programs},
	journal = {Declarative Programming {\textendash} Selected Papers from AGP 2000},
	volume = {48},
	year = {2001},
	note = {Available at URL: {\href{http://www.elsevier.nl/locate/entcs/volume48.html} {\texttt{http://www.elsevier.nl/locate/entcs/volume48.html}}}},
	pages = {1{\textendash}16},
	publisher = {Elsevier Science Publishers},
	abstract = {n this paper we define a new verification method based on an assertion language able to express properties defined by the user through a logic program. We first apply the verification framework defined in [CominiGLV99] to derive sufficient inductive conditions to prove partial correctness. Then we show how the resulting conditions can be proved using program transformation techniques.},
	keywords = {Abstract Interpretation, Inductive Verification, Transformation of logic programs},
	author = {Marco Comini and Roberta Gori and Giorgio Levi},
	editor = {Agostino Dovier and Maria Chiara Meo and Omicini, A.}
}
@proceedings {FPV01,
	title = {Time Limited Model Checking},
	journal = {Proceedings of International Workshop on Specification Analysis and Validation for Emerging Technologies in Computational Logic (SAVE{\textquoteright}01)},
	year = {2001},
	keywords = {cc, model checking},
	author = {Moreno Falaschi and Policriti, A. and Alicia Villanueva},
	editor = {Delzanno, G. and Etalle, S. and Gabbrielli, M.}
}
@proceedings {CominiDP99gulp,
	title = {Diagnosis of CHIP Programs Using Type Information},
	journal = {Appia-Gulp-Prode{\textquoteright}99, Joint Conference on Declarative Programming},
	year = {1999},
	pages = {337{\textendash}349},
	abstract = {This paper presents a diagnosis method for CLP, based on descriptive types. The method is applied to CLP language CHIP. To express type information, a restricted class of CLP programs is used. This class makes an abstract domain, for which most of the usual requirements are not satisfied. A concrete semantics is used which takes into account that CHIP uses syntactic unification and it does not implement the "classical" semantics of CLP.
Given a program and an approximate intended specification, our diagnosis algorithm finds all the clauses which are incorrect w.r.t the specification. No information about error symptoms is used. The algorithm reuses an abstract immediate consequence function from a type analysis system. The user does not have to provide whole specifications, their fragments can be submitted in an "on demand" way.},
	author = {Marco Comini and Drabent, W. and Pietrzak, P.},
	editor = {Maria Chiara Meo 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 {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.}
}
