@article {LV09b,
	title = {The tccp Interpreter},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {258},
	number = {1},
	year = {2009},
	pages = {63{\textendash}77},
	abstract = {The Timed Concurrent Constraint Language (tccp in short) is a constraint-based concurrent language inspired in process algebra. The language is well-suited for the specification of concurrent and reactive systems. tccp is parametric w.r.t. a constraint system, what is a main characteristic of the Concurrent Constraint Paradigm of Saraswat. Maude is an executable rewriting logic language specially well suited for the specification of distributed systems. The tccpInterpreter system is the result of implementing the tccp language (the constraint system, agents and semantics) in Maude. It parses the program and mimics in an automatic way its behavior allowing us to use the Maude features to execute and analyze tccp programs.},
	author = {Lescaylle, A. and Alicia Villanueva}
}
@article {LV09,
	title = {A Tool for Generating a Symbolic Representation of tccp Executions},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {246},
	year = {2009},
	pages = {131{\textendash}145},
	abstract = {
The Timed Concurrent Constraint language (tccp) was defined by F. de Boer et al. as an extension of the Concurrent Constraint Paradigm (Saraswat, 1993) for specifying reactive and embedded systems. In this paper, we describe the StructGenerator system which, given the specification of a tccp program, constructs a symbolic representation (a tccp Structure) modeling the behavior of such tccp program. The resulting structure allows one to verify the program by using a model-checking algorithm. It is similar to a Kripke Structure but, due to the nature of the ccp model, it differs from the classical approach in some important points that will be described along the paper. The StructGenerator system, implemented in C++, takes as input a file containing the specification of a tccp program and generates the associated tccp Structure. Along the paper, we cover the design and implementation of StructGenerator. We also demonstrate its functionality carrying out the execution of two practical examples.},
	author = {Lescaylle, A. and Alicia Villanueva}
}
@article {FLV08,
	title = {Formal Verification of Websites},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {200},
	number = {3},
	year = {2008},
	pages = {103{\textendash}118},
	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}
}
@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 {FLV07a,
	title = {Using Maude for the Formal Verification of Websites},
	journal = {Actas de las VII Jornadas de Programaci{\'o}n y Lenguajes (PROLE{\textquoteright}07)},
	year = {2007},
	month = {sep},
	pages = {71{\textendash}80},
	address = {Zaragoza (Spain)},
	abstract = {In this paper we address the problem of formal verification of websites by using declarative languages. In particular, we first define a model for websites which can intuitively be specified by using Maude. The model is defined to be 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 temporal logic which is used to specify properties of websites, and illustrate the kinds of properties that can be specified and verified by using the Maude model-checking tool. Finally, we have implemented a prototype by using the specification language Maude.},
	author = {Flores, S. and Salvador Lucas and Alicia Villanueva}
}
@proceedings {LV07,
	title = {Using tccp for the Specification and Verification of Communication Protocols},
	journal = {Proceedings of the 16th International Workshop on Funcional and (Constraint) Logic Programming (WFLP{\textquoteright}07)},
	year = {2007},
	pages = {169{\textendash}183},
	address = {Paris (France)},
	abstract = {The automatic analysis of cryptographic protocols by using formal methods on concurrent languages is a subject widely treated in the literature. From its beginning in the decade of the 70s, the field has been gaining maturity and consolidation. Some declarative approaches based on CLP, Haskell or Maude have been proposed for the specification and analysis of communication protocols. In this paper, we propose the Timed Concurrent Constraint Language (tccp in short) as the specification language for protocols. tccp is a declarative concurrent programming language which allows one to intuitively model concurrent and reactive systems. Cryptographic protocols can be specified in a very compact way
thanks to certain features of the language such as the non-deterministic behavior and concurrency. We show how to specify the basic actions that are usually performed during a protocol run. Thereafter, we show how to specify the participants in the protocol. Finally, we specify the intruder model by means of a hostile environment in which principals run the protocol. The model considered for the intruder is the popular model of Dolev-Yao. We use along the paper the Needham-Schroeder public key authentication protocol to illustrate the approach. The basic actions and the intruder implementation can be reused for the specification of many different protocols.},
	keywords = {tccp},
	author = {Lescaylle, A. and Alicia Villanueva}
}
@proceedings {LV07b,
	title = {Using tccp for the Specification of Communication Protocols},
	journal = {Actas de las VII Jornadas de Programaci{\'o}n y Lenguajes (PROLE{\textquoteright}07)},
	year = {2007},
	pages = {301{\textendash}310},
	address = {Zaragoza (Spain)},
	abstract = {The automatic analysis of cryptographic protocols by using formal methods on concurrent languages is a subject widely treated in the literature. From its beginning in the decade of the 70s, the field has been gaining maturity and consolidation. The Timed Concurrent Constraint Language (tccp in short) is a declarative concurrent programming language which, like other concurrent languages, allows us to intuitively model concurrent and reactive systems. In particular, cryptographic protocols can be specified in a very compact way thanks to certain features such as the non-determinism and concurrency, which are necessary to model such kind of systems. In this work, we show a method to specify cryptographic protocols using tccp. We have defined specifications for the actions that principals usually do during a protocol run. Moreover, we have defined a hostile environment in which agents run the protocol. The environment is actually the representation of the popular intruder model of Dolev-Yao. We use the Needham-Schroeder public key authentication protocol to illustrate the approach.},
	author = {Lescaylle, A. and Alicia Villanueva}
}
@proceedings {AGPV05c,
	title = {Verifying Real-Time Properties of tccp Programs},
	journal = {Proc. of the Quintas Jornadas sobre Programaci{\'o}n y Lenguajes, PROLE{\textquoteright}05, 2005},
	year = {2005},
	pages = {85{\textendash}94},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva},
	editor = {L{\'o}pez-Fraguas, F.J.}
}
@proceedings {ABEFL03b,
	title = {Abstract Correction of First-Order Functional Programs},
	journal = {12th International Workshop on Functional and Constraint Logic Programming, WFLP 2003},
	volume = {86},
	number = {3},
	year = {2003},
	publisher = {Elsevier},
	abstract = {Debussy is an (abstract) declarative diagnosis tool for functional
programs  which are written in OBJ style. The debugger  does not require
the user to either provide error symptoms in advance or answer any question
concerning program correctness. 

In this paper, we formalize an inductive learning  methodology
for repairing program bugs in OBJ-like programs.
Correct program rules are automatically synthesized 
from  examples which might be       
generated as an outcome by the Debussy diagnoser.},
	keywords = {Debugging, Inductive Learning, OBJ, program correction},
	author = {Maria Alpuente and Demis Ballis and Santiago Escobar and Moreno Falaschi and Salvador Lucas}
}
@proceedings {ABEFL03a,
	title = {Abstract Correction of OBJ-like Programs},
	journal = {Informl Proceeding of APPIA GULP PRODE 2003 (AGP 2003)},
	year = {2003},
	pages = {422{\textendash}433},
	author = {Maria Alpuente and Demis Ballis and Santiago Escobar and Moreno Falaschi and Salvador Lucas}
}
@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 {CominiGL00b,
	title = {Assertion based Inductive Verification Methods for Logic Programs},
	journal = {Proceedings of MFCSIT{\textquoteright}2000},
	volume = {40},
	year = {2001},
	note = {Available at URL: {\href{http://www.elsevier.nl/locate/entcs/volume40.html} {\texttt{http://www.elsevier.nl/locate/entcs/volume40.html}}}},
	pages = {1{\textendash}18},
	publisher = {Elsevier Science Publishers},
	abstract = {This paper is an overview of our results on the application of abstract interpretation concepts to the derivation of a verification method for logic programs. These include the systematic design of semantics modeling various proof methods and the characterization of assertions as abstract domains. We first apply the verification framework defined in [CominiGLV99] to derive inductive sufficient conditions for partial correctness. Then the domain of assertions is formalized as an abstract domain. We can therefore derive an assertion based verification method. We finally show two methods based on different assertion languages: a decidable assertion language and Horn clause logic used as assertion language.},
	keywords = {Abstract Interpretation, Assertion Language, Inductive Verification, Transformation of logic programs},
	author = {Marco Comini and Roberta Gori and Giorgio Levi},
	editor = {A. K. Seda}
}
@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.}
}
@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.}
}
@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 {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.}
}
@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.}
}
@proceedings {CominiL94,
	title = {An Algebraic Theory of Observables},
	journal = {Proceedings of the 1994 Int{\textquoteright}l Symposium on Logic Programming},
	year = {1994},
	pages = {172{\textendash}186},
	publisher = {The MIT Press},
	abstract = {We give an algebraic formalization of SLD-trees and their abstractions (observables). We can state and prove in the framework several useful theorems (AND-compositionality, correctness and full abstraction of the denotation, equivalent top-down and bottom-up constructions) about semantic properties of various observables. Observables are represented by Galois co-insertions and can be used to model abstract interpretation. The constructions and the theorems are inherited by all the observables which can be formalized in the framework. The power of the framework is shown by reconstructing some known examples (answer constraints, call patterns, correct call patterns and ground dependencies call patterns).},
	author = {Marco Comini and Giorgio Levi},
	editor = {Bruynooghe, M.}
}
