DSIC
Alicia Villanueva's research activity
UPV
 
Homepage
Research
Teaching
teaching
About
about
Links
links

Español English Italiano

I'm a member of the ELP research group

Research Interests
Declarative paradigm
The ELP group has traditionaly been devoted to the declarative paradigm. In particular, I've dealt with the Concurrent Constraint Paradigm. My PhD Thesis was centered in two languages from such paradigm. Currently, my interests are the tccp language (which is a timed concurrent constraint language able to represent reactive systems), functional and logic languages, and synchronous languages.
Model Checking
The ELP group is also interested in formal methods, in particular in lightweight formal methods. During the last years, I've been working on the Model Checking technique, which allows one to check whether a system model satisfies a given property. I'm also interested in other validation and verification techniques such as Software Testing or Debugging.
Abstract Interpretation
Formal Methods have a hugh temporal as well as spatial cost associated. For that reason, optimization techniques that allows one to reduce the search space are necessary. In particular, partial techniques such as abstract interpretation, or symbolic techniques such as the OBDD are commonly used. Abstract Interpretation has widely used in the literature to many ends. I'm interested in applying it to formal methods, making them lightweight and applicable to large programs.
Publications
International (electronic) Journals


         DATALOG_SOLVE: A Datalog-Based Demand-Driven Program Analyzer
with  María Alpuente, Marco Antonio Feliú and Christophe Joubert
          Electronic Notes in Theoretical Computer Science, Volume to appear, 2009
a
Abstract PDF BibTex

         A tool for Generating a Symbolic Representation of tccp executions
with  Alexei Lescaylle
          Electronic Notes in Theoretical Computer Science, Volume to appear, 2009
a
Abstract PDF BibTex

         Formal Verification of Websites
with Sonia Flores and Salvador Lucas
          Electronic Notes in Theoretical Computer Science, Volume 200, pages 103-118, 2008
a
Abstract PDF BibTex

         An Abstract Analysis Framework for Synchronous Concurrent Languages based on source-to-source transformation
 with María Alpuente, María del Mar Gallardo and Ernesto Pimentel
          Electronic Notes in Theoretical Computer Science, Volume 206, pages 3-21, 2008

 a
Abstract PDF BibTex

A Framework for the Timed Concurrent Constraint Programming with External Functions
with María Alpuente and Bernhard Gramlich
In Paqui Lucio, editor, Selected Papers from PROLE 2006
          Electronic Notes in Theoretical Computer Science, Volume 188C, pages 143-155, 2007
a
Abstract PDF PostScript BibTex

Verifying Real-Time Properties of tccp Programs
with María Alpuente, María del Mar Gallardo and Ernesto Pimentel
Journal of Universal Computer Science
          Volume 12, Issue 11, pages 1551-1573, 2006
a
Abstract  PDF PostScript BibTex

Automatic Verification of Timed Concurrent Constraint Programs
with Moreno Falaschi
Theory and Practice of Logic Programming. Volume 6, Issue 3. pages 265-300, May 2006
a
Abstract  PDF PostScript BibTex

A Semantic Framework for the Abstract Model Checking of tccp Programs
with María Alpuente, María del Mar Gallardo and Ernesto Pimentel
Special Issue on Quantitative Aspects of Programming Languages.
          Theoretical Computer Science, Volume 346, Issue 1, pages 58-95, November 2005
a
Abstract  PDF PostScript BibTex

Abstract Model Checking of tccp Programs
with María Alpuente, María del Mar Gallardo and Ernesto Pimentel
Proceedings of the 2nd Workshop on Quantitative Aspects of Programming Languages (QAPL 2004).
          Electronic Notes in Theoretical Computer Science, Volume 112, pages 19-36, January 2005
a
Abstract  PDF BibTex

Modeling Concurrent Systems Specified in a Temporal Concurrent Constraint language - I
with Moreno Falaschi and Alberto Policriti
In A. Dovier, M.C. Meo and A. Omicini, editors, Declarative Programming -- Selected Papers from AGP 2000. Volume 48 of Electronic Notes in Theoretical Computer Science, pages 197-210. Elsevier Science Publishers, 2001
a
Abstract  PDF PostScript BibTex


International Conferences and Workshops
Defining Datalog in Rewriting Logic
with  María Alpuente, Marco Antonio Feliú and Christophe Joubert
19th International Conference on Logic-based Program Synthesis and Transformation (LOPSTR'09)
Coimbra (Portugal) , 2009
See also the extended version
a
Abstract PDF BibTex

         Using Datalog and Boolean Equation Systems for Program Analysis
with  María Alpuente, Marco Antonio Feliú and Christophe Joubert
13rd International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008)
L'Acquila (Italy)
       Lecture Notes in Computer Science (LNCS), Volume 5596, 2009
a
Abstract PDF BibTex

A tool for Generating a Symbolic Representation of tccp executions
with Alexei Lescaylle
17th International Workshop on Funcional and (Constraint) Logic Programming (WFLP'08)
Siena (Italy) 2008
a
Abstract  PDF BibTex

Formal Verification of Websites
with Sonia Flores and Salvador Lucas
          3rd Internationall Workshop on Automated Specification and Verification of Web Systems (WWV 2007), Venezia (Italy), 2007
a
Abstract PDF BibTex

Using tccp for the Specification and Verification of Communication Protocols
with Alexei Lescaylle
Proceedings of the 16th International Workshop on Funcional and (Constraint) Logic Programming (WFLP'07), Paris (France) 2007
a
Abstract  PDF PostScript BibTex

AaAA Symbolic Model Checker for tccp Programs
with María Alpuente and Moreno Falaschi
Proceedings of the International Workshop on Rapid Integration of Software Ingeneering techniques, Lecture Notes in Computer Science (LNCS), Volume 3475, pages 45-56  May, 2005

Abstract  PDF PostScript BibTex

Symbolic Representation of tccp Programs
with María Alpuente and Moreno Falaschi
Proceedings of the 13th International Workshop on Funcional and (Constraint) Logic Programming (WFLP'04),  pages 104-117, Aachen (Germany) 2004
a
Abstract  PDF PostScript BibTex

Time Limited Model Checking
with Moreno Falaschi and Alberto Policriti
Proceedings of the International Workshop on Specification, Analysis and Validation for Emerging Technologies (SAVE), Cyprus 2001
a
Abstract  PDF PostScript BibTex

Modeling Concurrent Systems in a Temporal Concurrent Constraint language
with Moreno Falaschi and Alberto Policriti
Proceedings of the Joint Conference on Declarative Programming. University of "La Habana", Cuba 2000
a
Abstract  PDF PostScript BibTex

National Conferences and Workshops
Implementing Datalog in Maude
with  María Alpuente, Marco Antonio Feliú and Christophe Joubert
Actas del I Taller de Programación Funcional (TPF'09), San Sebastián (Spain) 2009
a
Abstract PDF BibTex

The tccp Interpreter
with Alexei Lescaylle
Actas de las IX Jornadas de Programación y Lenguajes (PROLE'09), San Sebastián (Spain) 2009
a
Abstract  PDF BibTex

Static Analysis of Java programs in a Rule-based Framework
with  María Alpuente, Marco Antonio Feliú and Christophe Joubert
VIII Jornadas sobre Programación y Lenguajes (PROLE 2008), Gijón (Spain) 2008
a
Abstract PDF BibTex

An Abstract Analysis Framework for Synchronous Concurrent Languages based on source-to-source Transformation
with María Alpuente, María del Mar Gallardo and Ernesto Pimentel
Actas de las VII Jornadas de Programación y Lenguajes (PROLE'07), Zaragoza (Spain) 2007
a
Abstract  PDF BibTex

Using Maude for the Formal Verification of Websites
with Sonia Flores and Salvador Lucas
Actas de las VII Jornadas de Programación y Lenguajes (PROLE'07), Zaragoza (Spain) 2007
a
Abstract  PDF BibTex

Using tccp for the Specification and Verification of Communication Protocols
with Alexei Lescaylle
Actas de las VII Jornadas de Programación y Lenguajes (PROLE'07), Zaragoza (Spain) 2007
a
Abstract  PDF BibTex

Timed Concurrent Constraint Programming with Instantaneous Computations
with María Alpuente and Bernhard Gramlich
Actas de las VI Jornadas de Programación y Lenguajes (PROLE'06), pags 253-262, Sitges (Spain) 2006
a
Abstract  PDF PostScript BibTex

Verifying Real-Time Properties of tccp Programs
with María Alpuente, María del Mar Gallardo and Ernesto Pimentel
Actas de las V Jornadas de Programación y Lenguajes (PROLE'05), pages 85-94, Granada (Spain) 2005
a
Abstract  PDF PostScript BibTex

A Semantic Framework for the Abstract Model Checking of tccp Programs (extended abstract)
with María Alpuente, María del Mar Gallardo and Ernesto Pimentel
Actas de las V Jornadas de Programación y Lenguajes (PROLE'05), pages 97-100, Granada (Spain) 2005
a
Abstract  PDF PostScript BibTex

Symbolic Model Checking for Timed Concurrent Constraint Programs
with María Alpuente and Moreno Falaschi
Actas de las III Jornadas de Programación y Lenguajes (PROLE'03), pages 151-165, Alicante (spain) 2003
a
Abstract  PDF PostScript BibTex


Technical Reports
Defining Datalog in Rewriting Logic
with María Alpuente, Marco A. Feliú and Christophe Joubert
Technical Report DSIC-II/07/09. DSIC, Universidad Politécnica de Valencia, 2009
a
PDF


Formal Verification of Websites
with Sonia Flores and Salvador Lucas
Technical Report DSIC-II/06/07. DSIC, Universidad Politécnica de Valencia, 2007
a
PDF

Timed Concurrent Constraint Programming with External Functions
with María Alpuente and Bernhard Gramlich
Technical Report DSIC-II/13/06. DSIC, Universidad Politécnica de Valencia, 2006

PDF

Symbolic Representation of tccp Programs
with María Alpuente and Moreno Falaschi
Technical Report DSIC-II/12/04. DSIC, Universidad Politécnica de Valencia, 2004

PostScript


PhD
Model Checking for the Concurrent Constraint Paradigm
PhD Thesis, Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, May 2003.
PhD Thesis, Dipartimento di Matematica e Informatica, Università degli Studi di Udine, May 2003.
*This PhD Thesis was done under a co-operation agreement (cotutela) between the two universities.

Abstract  PDF PostScript BibTex

Model Checking for the Concurrent Constraint Paradigm (Phd Abstract)
Bulletin of the European Association for Theoretical Computer Science EATCS, Number 82, pages 389-392, February 2004.

Abstract  PDF PostScript BibTex

Model Checking for the Concurrent Constraint Paradigm (Phd Abstract)
The European Journal on Artificial Intelligence. AI Communications, Volume 17, Number 2, pages 93-94, 2004.

Abstract  PDF PostScript BibTex


Software
The tccp interpreter: available here
The tccp-func interpreter: the interpreter is being re-implemented. The old version is still available  here
The tccp model checker: a preliminary version is available. If you need it, please contact Alexei Lescaylle or myself.

Co-Authors

Last Update: November 2009