@proceedings {BacciCFV12-ICLP,
	title = {The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages},
	journal = {ICLP (Technical Communications)},
	volume = {To appear},
	year = {2012},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum Fuer Informatik},
	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.},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva}
}
@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 {BacciCFV12,
	title = {Automatic Synthesis of Specifications for First Order Curry Programs},
	journal = {Proceedings of the 14th symposium on Principles and practice of declarative programming},
	year = {2012},
	pages = {25{\textendash}34},
	publisher = {ACM},
	address = {New York, NY, USA},
	abstract = {This paper presents a technique to automatically infer algebraic property-oriented specifications from first-order Curry programs. Curry is a lazy functional logic language and the interaction between laziness and logical variables raises some additional difficulties with respect to other proposals for functional languages. 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. We propose a (glass-box) semantic-based inference method which relies on a fully-abstract (condensed) semantics for achieving, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.},
	keywords = {Curry, property-oriented specifications, semantic-based inference methods},
	isbn = {978-1-4503-1522-7},
	doi = {10.1145/2370776.2370781},
	url = {http://doi.acm.org/10.1145/2370776.2370781},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva}
}
@article {CominiTV11absdiag,
	title = {Abstract Diagnosis for Timed Concurrent Constraint programs},
	journal = {Theory and Practice of Logic Programming},
	volume = {11},
	number = {4-5},
	year = {2011},
	month = {2011},
	pages = {487--502},
	abstract = {The Timed Concurrent Constraint Language (tccp in short) is a concurrent logic language based on the simple but powerful concurrent constraint paradigm of Saraswat. In this paradigm, the notion of store-as-value is replaced by the notion of store-as-constraint, which introduces some differences w.r.t. other approaches to concurrency.

In this paper, we provide a general framework for the debugging of tccp programs. To this end, we first present a new compact, bottom-up semantics for the language that is well suited for debugging and verification purposes in the context of reactive systems. We also provide an abstract semantics that allows us to effectively implement debugging algorithms based on abstract interpretation.

Given a tccp program and a behavior specification, our debugging approach automatically detects whether the program satisfies the specification. This differs from other semi-automatic approaches to debugging and avoids the need to provide symptoms in advance. We show the efficacy of our approach by introducing an application example. We choose a specific abstract domain and show how we can detect that a program is erroneous.},
	url = {http://users.dimi.uniud.it/~marco.comini/Papers/AbsDiagTCCP/AbsDiagTCCP11.pdf},
	author = {Marco Comini and Laura Titolo and Alicia Villanueva}
}
@proceedings {BacciCFV11,
	title = {Automatic Synthesis of Specifications for Curry Programs},
	journal = {Logic-based Program Synthesis and Transformation, 21th International Symposium {\textendash} Pre-Proceedings},
	year = {2011},
	note = {To appear},
	publisher = {Springer-Verlag},
	address = {Odense, Denmark},
	abstract = {This extended abstract presents a technique to automatically infer specifications from Curry programs. Program specifications (in particular, automatically derived specifications) have been used for program verification, understanding, documentation, service discovering or testing. Our technique, statically infers from the source code of a Curry program a specification which consists of a set of semantic properties that the program operations satisfy. These properties are given by means of equations relating (nested) operation calls that have the same behavior. Our method relies on the semantics of [<a href="http://flit.dimi.uniud.it/?q=biblio/baccic10conc">1</a>] for achieving, to some extent, the correctness of the inferred specification, as opposed to other similar tools based on testing.
In this paper, we present the main ideas of the approach emphasizing the difficulties addressed for the case of the Curry language.},
	keywords = {Abstract Interpretation, Algebraic-oriented Specification, Curry},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva}
}
@article {CominiTV11sem,
	title = {A Compact Goal-Independent Bottom-Up Fixpoint Modeling the Behavior of tccp},
	number = {DIMI-UD/01/2011/RR},
	year = {2011},
	publisher = {Dipartimento di Matematica e Informatica, U. di Udine},
	abstract = {The Timed Concurrent Constraint Language (tccp in short) is a concurrent logic language based on the simple but powerful concurrent constraint paradigm of Saraswat. In this paradigm, the notion of store-as-value is replaced by the notion of store-as-constraint, which introduces some dierences w.r.t. other approaches to concurrency.
In this work, we present a new compact, bottom-up semantics for the language that is well suited for abstract interpretation based debugging and verication purposes in the context of reactive systems. The defined semantics is shown to be correct w.r.t. the behavior of tccp. 
We also propose a an abstract semantics that allows us to effectively implement debugging algorithms based on abstract interpretation. This semantics keeps the particular strong synchronization characteristic of the language.},
	url = {http://users.dimi.uniud.it/~marco.comini/Papers/BotUpBehaTCCP/BotUpBehaTCCP11.pdf},
	author = {Marco Comini and Laura Titolo and Alicia Villanueva}
}
@proceedings {AFJV09a,
	title = {Defining Datalog in Rewriting Logic},
	journal = {Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR{\textquoteright}09)},
	volume = {6037},
	year = {2010},
	pages = {188{\textendash}204},
	publisher = {Springer-Verlag},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva},
	editor = {Schreye, D. de}
}
@article {AFJV09b,
	title = {DATALOG_SOLVE: A Datalog-Based Demand-Driven Program Analyzer},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {248},
	year = {2009},
	pages = {57{\textendash}66},
	abstract = {This work presents a practical Java program analysis framework that is obtained by combining a Java virtual
machine with a general-purpose verification toolbox that we previously extended. In our methodology,
Datalog clauses are used to specify complex interprocedural program analyses involving dynamically created
objects. After extracting an initial set of Datalog constraints about the Java bytecode program semantics,
our framework transforms the Datalog rules of a particular analysis into a Boolean Equation System (Bes),
whose local resolution using the aforementioned extended verification toolbox corresponds to the demand-
driven computation of the analysis.},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva}
}
@article {AFJV09tr,
	title = {Defining Datalog in Rewriting Logic},
	number = {DSIC-II/07/09},
	year = {2009},
	publisher = {DSIC, Universidad Polit{\'e}cnica de Valencia},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva}
}
@proceedings {AFJV09,
	title = {Implementing Datalog in Maude},
	journal = {Proceedings of the IX Jornadas sobre Programaci{\'o}n y Lenguajes (PROLE{\textquoteright}09) and I Taller de Programaci{\'o}n Funcional (TPF{\textquoteright}09)},
	year = {2009},
	month = {September},
	pages = {15{\textendash}22},
	abstract = {Transformation of programs among different paradigms has been widely studied in academic research and education. The interest on Datalog has recently increased as a specification language for expressing, in just a few lines, complex interprocedural analyses involving dynamically created objects. In real-world problems, the Datalog rules encoding a particular analysis must be solved generally under a huge set of Datalog facts that are automatically extracted from the analyzed program (e.g. pointer dependencies). In that context, this work aims at exploiting Maude{\textquoteright}s capabilities for supporting efficient evaluation of Datalog queries. We demonstrate how, starting from an almost straightforward transformation of Datalog programs into Maude specifications, we are able to achieve a highly efficient version.},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva},
	editor = {Pe{\~n}a, R.}
}
@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}
}
@proceedings {AFJV08,
	title = {Using Datalog and Boolean Equation Systems for Program Analysis},
	journal = {Proceedings of the 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS{\textquoteright}08)},
	volume = {5596},
	year = {2009},
	pages = {215{\textendash}231},
	publisher = {Springer-Verlag},
	abstract = {This paper describes a powerful, fully automated method to evaluate Datalog queries by using Boolean Equation Systems (Bess), and its application to object-oriented program analysis. Datalog is used as a specification language for expressing complex interprocedural program analyses involving dynamically created objects. In our methodology, Datalog rules encoding a particular analysis together with a set of constraints (Datalog facts that are automatically extracted from program source code) are dynamically transformed into a Bes, whose local resolution corresponds to the demand-driven evaluation of the program analysis. This approach allows us to reuse existing general purpose verification toolboxes, such as Cadp, providing local Bes resolutions with linear-time complexity. Our evaluation technique has been implemented and successfully tested on several Java programs and Datalog analyses that demonstrate the feasibility of our approach.},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva},
	editor = {Darren Cofer and Alessandro Fantechi}
}
@article {AGPV08,
	title = {An Abstract Analysis Framework for Synchronous Concurrent Languages based on source-to-source Transformation},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {206},
	year = {2008},
	pages = {3{\textendash}21},
	abstract = {A pretty wide range of concurrent programming languages have been developed over the years. Coming from different programming traditions, concurrent languages differ in many respects, though all share the common aspect to expose parallelism to programmers. In order to provide language level support to programming with more than one process, a few basic concurrency primitives are often combined to provide the main language constructs, sometimes making different
assumptions. In this paper, we analyze the most common primitives and related semantics for the class of synchronous concurrent programming languages, i.e., languages with a global mechanism of processes synchronization. Then, we present a generic framework for approximating the semantics of the main constructs which applies to both, declarative as well as imperative concurrent programming languages. We determine the conditions which ensure the correctness of the approximation, so that the resulting abstract semantics safely supports program analysis and verification. Finally, we ascertain the conditions that make it possible to implement the abstraction by a source to source transformation of the language semantics.},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. 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 {AGPV07,
	title = {An Abstract Analysis Framework for Synchronous Concurrent Languages based on source-to-source Transformation},
	journal = {Actas de las VII Jornadas de Programaci{\'o}n y Lenguajes (PROLE{\textquoteright}07)},
	year = {2007},
	month = {sep},
	pages = {81{\textendash}92},
	abstract = {A pretty wide range of concurrent programming languages have been developed over the years. Coming from different programming traditions, concurrent languages differ in many respects, though all share the common aspect to expose parallelism to programmers. In order to provide language level support to programming with more than one process, a few basic concurrency primitives are often combined to provide the main language constructs, sometimes making different
assumptions. In this paper, we analyze the most common primitives and related semantics for the class of synchronous concurrent programming languages, i.e., languages with a global mechanism of processes synchronization. Then, we present a generic framework for approximating the semantics of the main constructs which applies to both, declarative as well as imperative concurrent programming languages. We determine the conditions which ensure the correctness of the approximation, so that the resulting abstract semantics safely supports program analysis and verification. Finally, we ascertain the conditions that make it possible to implement the abstraction by a source to source transformation of the language semantics.},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. 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.}
}
@article {AGV07,
	title = {A Framework for Timed Concurrent Constraint Programming with External Functions},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {188C},
	year = {2007},
	pages = {143{\textendash}155},
	abstract = {The Timed Concurrent Constraint programming language (tccp in short),  was introduced for modeling reactive systems. This language allows one to model in a very intuitive way typical ingredients of  these systems such as timeouts, preemptions, etc. However, there is no natural way for modeling other desirable features such as functional computations, for example for calculating arithmetic results. In fact, although it is certainly possible to implement such kind of operations,  each single step of the computation takes time in tccp, and avoiding interferences with the intended overall behavior of the (reactive) system is quite involved.

In this paper, we propose an extension of tccp for modeling instantaneous computations which  improves the  expressiveness of the language, in the sense that operations that are cumbersome to implement in pure tccp, are executed by calling an efficient, external functional engine, while the tccp programmer can focus on the pure, and usually more complex, reactive part of the system. We also describe a case study which motivates the work, and discuss how the new capability presented here can also be used as a new tool for developers from the verification point of view.},
	keywords = {functions, tccp},
	author = {Maria Alpuente and Gramlich, B. and Alicia Villanueva}
}
@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}
}
@article {FV06,
	title = {Automatic Verification of Timed Concurrent Constraint programs},
	journal = {Theory and Practice of Logic Programming},
	volume = {6},
	number = {3},
	year = {2006},
	pages = {265{\textendash}300},
	keywords = {cc, model checking},
	author = {Moreno Falaschi and Alicia Villanueva}
}
@article {AGPV06,
	title = {A Real-Time Logic for tccp verification},
	journal = {Journal of Universal Computer Science},
	volume = {12},
	number = {11},
	year = {2006},
	month = {November},
	pages = {1551{\textendash}1573},
	keywords = {cc, Logic},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva}
}
@article {AGV06-tr,
	title = {Timed Concurrent Constraint programming with External Functions},
	number = {DSIC-II/13/06},
	year = {2006},
	publisher = {DSIC, UPV},
	author = {Maria Alpuente and Gramlich, B. and Alicia Villanueva}
}
@proceedings {AGV06,
	title = {Timed Concurrent Constraint Programming with Instantaneous Computations},
	journal = {Actas de las VI Jornadas de Programaci},
	year = {2006},
	address = {Sitges, Barcelona, Spain},
	author = {Maria Alpuente and Gramlich, B. and Alicia Villanueva}
}
@article {AGPV05,
	title = {A Semantic Framework for the Abstract Model Checking of tccp programs},
	journal = {{Theoretical Computer Science}},
	volume = {346},
	year = {2005},
	pages = {58{\textendash}95},
	keywords = {Abstraction, cc, model checking},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva}
}
@inbook {AFV04,
	title = {A Symbolic Model checker for tccp Programs},
	booktitle = {Proceedings of the International Workshop on Rapid Integration of Software Ingeneering techniques (RISE{\textquoteright}04)},
	series = {Lecture Notes in Computer Science},
	volume = {3475},
	year = {2005},
	pages = {45{\textendash}56},
	publisher = {Springer Verlag},
	organization = {Springer Verlag},
	keywords = {cc, model checking, symbolic representation},
	author = {Maria Alpuente and Moreno Falaschi 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.}
}
@article {AGPV04,
	title = {Abstract Model Checking of tccp programs},
	journal = {Electronic Notes in Theoretical Computer Science (ENTCS)},
	volume = {112},
	year = {2004},
	pages = {19{\textendash}36},
	keywords = {Abstraction, cc, model checking},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva}
}
@proceedings {AFV03b,
	title = {Symbolic Model Checking for Timed Concurrent Constraint Programs},
	journal = {Proceedings of the III Jornadas de Programaci{\'o}n y Lenguajes},
	year = {2003},
	address = {Alicante},
	keywords = {cc, model checking, symbolic representation},
	author = {Maria Alpuente and Moreno Falaschi and Alicia Villanueva}
}
@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.}
}
@article {FPV00b,
	title = {Modeling Timed Concurrent systems in a Temporal Concurrent Constraint language - I},
	journal = {Electronic Notes in Theoretical Computer Science (ENTCS)},
	volume = {48},
	year = {2000},
	pages = {1{\textendash}15},
	keywords = {cc, model checking},
	author = {Moreno Falaschi and Policriti, A. and Alicia Villanueva}
}
@proceedings {FPV00a,
	title = {Modeling Timed Concurrent systems in a Temporal Concurrent Constraint language},
	journal = {Proceedings of the 2000 Joint Conference on Declarative Programming},
	year = {2000},
	publisher = {University of La Habana},
	address = {La Habana, Cuba},
	keywords = {cc, model checking},
	author = {Moreno Falaschi and Policriti, A. and Alicia Villanueva}
}
