DSIC
Attività di ricerca di Alicia Villanueva
UPV
 
Homepage
Research
Didattica
teaching
Varie
about
Links
links

Español English Italiano

Sono membro del gruppo di ricerca ELP
15th International Static Analysis Symposium (SAS 2008)   
To be held in Valencia (Spain), July 16-18, 2008

Interessi di ricerca
Paradigma Dichiarativo
Il gruppo ELP ha lavorato storicamente nello studio e sviluppo del paradigma dichiarativo. Io ho lavorato nell'ambito del paradigma concorrente con vincoli (Concurrent Constraint Paradigm). La mia tesi di dottorato  si è centrata in due linguaggi di programmazione appartenenti a questo paradigma. Attualmente sono interessata nel linguaggio tccp (che si tratta di un linguaggio concorrente con i vincoli ma temporizzato, il quale è capace di modellare sistemi reattivi), in linguaggi funzionali e logici, e in linguaggi sincroni.
Model Checking
Il gruppo ELP si è anche interessato nei metodi formali. In particulare nella versione lightweight di questi metodi. Durante gli ultimi anni, ho studiato ed applicato la tecnica del Model Checking, la quale ci permette di verificare se un dato sistema soddisfa una propietà specificata. Sono anche interessata in altre techniche di validazione, verifica e testing come il Software Testing o il Debugging.
Interpretazione Astratta
I metodi formali hanno per definizione una complessita temporale e anche spaziale troppo elevata. È per questo che le technique di optimizazione diventano importanti in questo contesto. Queste technique ci permettono di ridurre lo spazio di ricerca. Di solito si applicano technique parziali come la interpretazione astratta, ma anche technique simboliche come la representazione basata sugli OBDD. La interpretazione astratta si è usata ampiamente nella literatura con molto diversi obiettivi. Io sono interessata nell'applicare questa technica ai metodi formali, facendogli agili e capaci di lavorare con grandi programmi.
Pubblicazioni
Riviste (elettroniche) internazionali

         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


Conferenze e Workshop Internazionali
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
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

Conferenze e Workshop Nazionali
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
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 Thesis
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-Autori

Last Update: Luglio 2009