@proceedings {FLV07b,
	title = {Formal Verification of Websites},
	journal = {Proceedings of the 16th International Workshop on Automated Specification and Verification of Web Sites (WWV{\textquoteright}07)},
	year = {2007},
	month = {dec},
	pages = {83{\textendash}97},
	address = {San Servolo, Venice, Italy},
	abstract = {In this paper, a model for websites is presented. The model is well-suited for the formal verification of dynamic as well as static properties of the system. A website is defined as a collection of web pages which are semantically connected in some way. External web pages (which are related pages not belonging to the website) are treated as the environment of the system. We also present the logic which is used to specify properties of websites, and illustrate the kinds of properties that can be specified and verified by using a model-checking tool on the system. In this setting, we discuss some interesting properties which often need to be checked when designing websites. We have encoded the model using the specification language Maude which allows us to use the Maude model-checking tool.},
	author = {Flores, S. and Salvador Lucas and Alicia Villanueva},
	editor = {Demis Ballis and Santiago Escobar and Marchiori, M.}
}
@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.}
}
@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.}
}
@article {CominiM96,
	title = {Compositionality properties of {\i}t SLD-derivations},
	journal = {Theoretical Computer Science},
	volume = {211},
	number = {1-2},
	year = {1999},
	pages = {275{\textendash}309},
	abstract = {The paper introduces a semantics for definite logic programs expressed in term of SLD-derivations and studies various properties of SLD-derivations by using the above semantics. The semantics of a program is a goal-independent denotation, which can equivalently be specified by a denotational semantics and a transition system. The denotation is proved to be correct, minimal, AND-compositional and OR-compositional. The denotational semantics and the transition system are defined in terms of a set of primitive semantic operators, whose properties are directly related to the properties of the denotation. The SLD-derivations semantics has been designed to act as collecting semantics for a framework of abstract semantics in the literature.},
	author = {Marco Comini and Maria Chiara Meo}
}
@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 {CominiLM95,
	title = {Compositionality of SLD-derivations and their abstractions},
	journal = {Proceedings of the 1995 Int{\textquoteright}l Symposium on Logic Programming},
	year = {1995},
	pages = {561{\textendash}575},
	publisher = {The MIT Press},
	abstract = {We define a semantic framework to reason about compositional properties of SLD-derivations and their abstractions (observables). 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 and minimality). This leads us to a flexible classification of the observables, where we can reason about properties such as OR-compositionality and existence of abstract transition system. 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.},
	author = {Marco Comini and Giorgio Levi and Maria Chiara Meo},
	editor = {Lloyd, J.}
}
