@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 {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}
}
@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}
}
@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 {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}
}
@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 {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 {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}
}
@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 {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.}
}
