Papers of the ELP Group

This document lists some recent papers of the ELP Group.

Papers are organized in three groups:

Journal and Conference papers
PhD Theses
Technical Reports

They are ordered by year of publication and author(s) (inverse ordering). In most cases you can retrieve, just by clicking, the abstracts of the papers, their DVI, PDF and PostScript versions as well as the corresponding BibTeX entries.

© Copyright

Copyrights are held variously by the authors or publishers. In general, these papers are provided for direct use in scholarship and education. If you are contemplating other uses, such as republication, you must obtain appropriate permissions. If you wish to cite any of the published work, please look up the formal publication, and use that version. The preprints in this area are as accurate as we can make them, but they are not authoritative copies of the published versions.

2012

• M. Alpuente, D. Ballis, F. Frechina, D. Romero
  Backward Trace Slicing for Conditional Rewrite Theories
  The 18th Int'l Conf. on Logic for Programming, Artificial Intelligence and Reasoning
  LPAR-18 (Mérida, Venezuela), Mar 2012
  LNCS, To appear 2012
  © Springer-Verlag
  Available:
  

2011

• M. Alpuente (editor)
  Logic-based Program Synthesis and Transformation, 20th International  Symposium
  LOPSTR 2010 (Hagenberg, Austria), Jul 2008.
  LNCS 6564, 2011
  © Springer-Verlag
  Available:  DOI link
  
  
• M. Alpuente, D. Ballis, J. Espert, D. Romero
  Backward Trace Slicing for Rewriting Logic Theories
  23rd International Conference on Automated Deduction, CADE 2011
  Wrocław, Poland, 31 July – 5 August 2011
  LNCS 6803, To appear 2011
  © Springer-Verlag
  Available:  PDF
  
  
• M. Alpuente, D. Ballis, J. Espert,  F. Frechina, D. Romero
  Debugging of Web Applications with WEB-TLR
  7th Int'l Workshop on Automated Specification and Verification of Web Systems (WWV2011).
  June 9, 2011. Reykjavik, Iceland.
  © EPTCS (Electronic Proceedings in Theoretical Computer Science), To appear 2011
  Available:  PDF
  
  
• M. Alba, M. Alpuente, S. Escobar
  Approximating Non-interference  and Erasure in Rewriting Logic
  12th International Symposium on Symbolic and Numeric Algorithms for Scientific
  Computing SYNASC 2010
  Timisoara (Romania), September 23-26, 2010  
  © IEEE Computer Society Press, pages 124-132, 2011
  Available:  PDF
  
  
• M. Alpuente, M. Baggi, D. Ballis,  M. Falaschi
  Completeness of Unfolding for Rewriting Logic Theories
  12th International Symposium on Symbolic and Numeric Algorithms for Scientific
  Computing SYNASC 2010
  Timisoara (Romania), September 23-26, 2010
  © IEEE Computer Society Press, pages 116-123, 2011
  Available:  PDF
  
  
• M. Alpuente, M. Feliu, C. Joubert, A. Villanueva
  Datalog-based Program Analysis with BES and RWL
  Datalog 2.0: The resurgence of Datalog in Academia and Industry
  LNCS 6702, To appear 2011
  © Springer-Verlag
  Available:  PDF
   
  
  

• M. Alba, M. Alpuente, S. Escobar
  Confidentiality Certification of source Java code in JavaPCC
  10th International Workshop on Automated Verification of Critical Systems (AVOCS 2010)
  Available:  PDF
  

• M. Alba, M. Alpuente, S. Escobar
  Abstract Certification of Global Non-Interference in Rewriting Logic
  Formal Methods for Components and Objects
  (Selected and revised papers from FMCO 2009)
  LNCS 6286: 105-124, 2010.
  © Springer-Verlag
  Available: DOI PDF CoRR with proofs
  
  
• M. Alpuente, M. Baggi, D. Ballis,  M. Falaschi
  A Fold/Unfold Transformation Framework for Rewrite Theories extended to CCT
  ACM SIGPLAN 2010 Workshop on Partial Evaluation and Program Manipulation PEPM'10
  Madrid (Spain), January 2010, pp. 43-52
  © ACM Press
  Available:  PDF
  
  
• M. Alpuente, D. Ballis, F. Correa, and M. Falaschi
  An Integrated Framework for the Diagnosis and Correction of Rule-Based Programs
  Theoretical Computer Science 411(47): 4055-4101, 2010.
  © Elsevier
  Available: DOI link Preliminary version
  
  
• M. Alpuente, D. Ballis, J. Espert,  D. Romero
  Model-checking Web Applications with Web-TLR
  8th International Symposium on Automated Technology for Verification and Analysis,
  ATVA 2010 Singapore, September 21-24, 2010
  LNCS 6252: 341-346, 2010
  © Springer-Verlag
  Available:  PDF
  
  
• M. Alpuente, D. Ballis,  M. Falaschi
  Transformation and Debugging of Functional Logic Programs
  25 Years of Logic Programming in Italy
  LNCS 6125: 271-299, 2010. Chapter XV.
  © Springer-Verlag
  Available:  PDF
  
  
• M. Alpuente, M. Comini, S. Escobar, M. Falaschi, and J. Iborra
  A Compact Fixpoint Semantics for Term Rewriting Systems
  Theoretical Computer Science, 411(37):3348-3371, 2010.
  © Elsevier
  Available: DOI link Preliminary version
  
  
• M. Alpuente, S. Escobar, B. Gramlich, and S. Lucas
  On-Demand Strategy Annotations Revisited: An Improved On-Demand Evaluation Strategy
  Theoretical Computer Science, 411(2):504-542, 2010.
  © Elsevier
  Available: DOI link Preliminary version
  
  
• M. Alpuente, S. Escobar, J. Iborra
  Modular Termination of Basic Narrowing and Equational Unification
  Journal of IGPL
  © Oxford U. Press
  Available: DOI link Preliminary version
  
  
• M. Alpuente, M. Feliu, C. Joubert, A. Villanueva
  Defining Datalog in Rewriting Logic
  Logic-Based Program Synthesis and Tranformation
  (Selected and revised papers from LOPSTR 2009)
  LNCS 6037: 188-204, 2010
  © Springer-Verlag
  Available:  PDF
  
  
• M. Alpuente, D. Romero
  A Tool for Computing the Visual Similarity of Web Pages
  2010 International Symposium on Applications and the Internet
  SAINT 2010 (Seoul, Korea), Jul 2010, pp. 45-51.
  © IEEE Computer Society Press, 2010
  Available:  PDF
  
  

2009

• M. Alba, M. Alpuente, S. Escobar
  Automatic Certification of Non-Interference in Rewriting Logic
  Formal Methods for Industrial Critical Systems
  (Selected and revised papers from FMICS 2008)
  LNCS 5596: 182-198, 2009.
  © Springer-Verlag
  Available: DOI link PDF
  

• M. Alba, M. Alpuente, S. Escobar, P. Ojeda, and D. Romero
  A Tool for Automated Certification of Java Source Code in Maude
  Electronic Notes in Theoretical Computer Science 248:19-29, 2009
  © Elsevier
  Available: DOI link PDF
  
  
• M. Alpuente  D. Ballis, and D. Romero 
  Specification and Verification of Web Applications in Rewriting Logic
  16th Int'l Symposium on Formal Methods FM 2009
  Eindhoven (NL), November 2009
  LNCS 5850: 790:805, 2009.
  © Springer-Verlag
  Available: PDF
  
  
• M. Alpuente, B. Cook, C. Joubert (editors)
  Formal Methods for Industrial Critical Systems, 14th International  Symposium
  FMICS 2009 (Eindhoven, The Netherlands), November 2009.
  LNCS 5825, 2009
  © Springer-Verlag
  Available:  DOI link
  
  
• M. Alpuente, S. Escobar, J. Iborra
  Termination of Narrowing Revisited
  Theoretical Computer Science 410(46): 4608-4625, 2009.
  © Elsevier
  Available: DOI link Preliminary version
  
  
• M. Alpuente, S. Escobar, J. Meseguer, P. Ojeda
  Order-sorted Generalization
  (Selected and revised papers from WFLP 2008)
  Electronic Notes in Theoretical Computer Science, 246:27-38, 2009
  © Elsevier
  Available: DOI link PDF
  
  
• M. Alpuente, S. Escobar, J. Meseguer, P. Ojeda
  A Modular Equational Generalization Algorithm
  Logic-Based Program Synthesis and Tranformation
  (Selected and revised papers from LOPSTR 2008)
  LNCS 5438:24:38, 2009.
  © Springer-Verlag
  Available: DOI link PDF
  

• M. Alpuente, M. Feliu, C. Joubert, A. Villanueva
  DATALOG_SOLVE: A Datalog-Based Demand-Driven Program Analyzer
  Electronic Notes in Theoretical Computer Science,  248:57-66, 2009
  © Elsevier Science
  Available:  PDF
  
  
• M. Alpuente, M. Feliu, C. Joubert, A. Villanueva
  Using Datalog and Boolean Equation Systems for Program Analysis
  Formal Methods for Industrial Critical Systems
  (Selected and revised papers from FMICS 2008)        
  LNCS 5596: 215-231, 2009.
  © Springer-Verlag
  Available:  PDF
  

• M. Alpuente and D. Romero
  A Visual Technique for Web Pages Comparison
  Electronic Notes in Theoretical Computer Science 235:3-18, 2009
  © Elsevier Science
  Available:  PDF
  
  

2008

• B. Alarcon and S. Lucas
  Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting
  8th Spanish Conference on Programming and Computer Languages
  PROLE 2008 (Gijón, Spain), Oct 2008.
  Electronic Notes in Theoretical Computer Science, To appear 2008.
  © Elsevier
  Available: Abstract / PDF

• M. Alba, M. Alpuente, S. Escobar
  Automatic Certification of Java Source Code in Rewriting Logic
  12th Int'l Workshop on Formal Methods for Industrial Critical Systems
  FMICS 2007 (Berlin, Germany), Jul 2007. 
  LNCS 4916:200-216, 2008.
  © Springer-Verlag
  Available:  PDF
  
  
• M. Alpuente, M. Baggi, D. Ballis, M. Falaschi
  Semantic Verification of Web System Contents
  Fifth International ER Workshop on Web Information Systems Modeling
  WISM 2008 (Barcelona, Spain), Oct 2008.
  LNCS 5232:437-446, 2008
  © Springer-Verlag
  Available:  PDF
  
  
• M. Alpuente, D. Ballis, M. Falaschi, P. Ojeda, D. Romero
  An Abstract Generic Framework for Web Site Verification
  2008 International Symposium on Applications and the Internet
  SAINT 2008 (Turku, Finland), Jul 2008.
  © IEEE Computer Society Press, 2008
  Available: PDF
  
  
• M. Alpuente, S. Escobar, J. Iborra
  Termination of Narrowing using Dependency Pairs
  24th Int'l Conf. on Logic Programming
  ICLP 2008 (Udine, Italy), Dec 2008.
  LNCS 5366: 317-331, Dec 2008.
  © Springer-Verlag
  Available: DOI link PDF
  
  
• M. Alpuente, S. Escobar, J. Iborra
  Modular Termination of Basic Narrowing
  19th Int'l Conf. on Rewriting Techniques and Applications
  RTA 2008 (Hagenberg, Austria), Jul 2008.
  LNCS 5117:1-16, Jul 2008
  © Springer-Verlag
  Available:  PDF
  
  
• M. Alpuente, S. Escobar, J. Meseguer, P. Ojeda
  A Modular Equational Generalization Algorithm
  18th Int'l Symp. on Logic Based Program Synthesis and Tranformation
  LOPSTR 2008, Valencia (Spain), Jul 2008
  © Springer-Verlag
  Available:  PDF
  

• M. Alpuente, M. M. Gallardo, E. Pimentel, A. Villanueva
  An Abstract Analysis Framework for Synchronous Concurrent Languages
  based on source-to-source Transformation
  Electronic Notes in Theoretical Computer Science, Vol 206C:3-21
  © Elsevier Science
  Available:  PDF
  
  
• M. Alpuente, G. Vidal (editors)
  15th International Static Analysis Symposium
  SAS 2008 (Valencia, Spain), Jul 2008.
  LNCS 5079, 2008
  © Springer-Verlag
  Available:  DOI link
  

• F. Duran, S. Lucas, ,C. Marche, J. Meseguer, and X. Urbain
  Proving Operational Termination of Membership Equational Programs
  Higher-Order and Symbolic Computation, 21(1-2):59-88, June 2008.
  © Springer-Verlag
  Available: Abstract / PDF

• F. Duran, S. Lucas, J. Meseguer
  Methods for proving termination of rewriting-based programming languages
  8th Spanish Conference on Programming and Computer Languages, PROLE'08
  Electronic Notes in Theoretical Computer Science, 2008, to appear
  © Elsevier
  Available: Abstract / PDF

• F. Duran, S. Lucas, J. Meseguer
  MTT: The Maude Termination Tool
  4th International Joint Conference on Automated Reasoning, IJCAR'08
  LNAI to appear, 2008.
  © Springer-Verlag
  Available: Abstract / PDF

• F. Duran, S. Lucas, J. Meseguer
  Web Services and Interoperability for the Maude Termination Tool
  8th Spanish Conference on Programming and Computer Languages, PROLE'08
  Electronic Notes in Theoretical Computer Science, 2008, to appear
  © Elsevier
  Available: Abstract / PDF

• S. Escobar, C. Meadows, J. Meseguer.
  State Space Reduction in the Maude-NRL Protocol Analyzer
  In proceedings of 13th European Symposium on Research in Computer Security (ESORICS08),
  LNCS to appear, 2008
  © Springer-Verlag
  

• S. Escobar, J. Meseguer, R. Sasse.
  Effectively Checking or Disproving the Finite Variant Property
  In proceedings of 19th International Conference on Rewriting Techniques and Applications (RTA'08),
  LNCS to appear, 2008
  © Springer-Verlag
  

• S. Escobar, J. Meseguer, R. Sasse.
  Variant Narrowing and Equational Unification
  In proceedings of 7th International Workshop on Rewriting Logic and its Applications (WRLA08),
  Electronic Notes in Theoretical Computer Science, 2008, to appear
  © Elsevier
  

• S. Flores, S. Lucas and A. Villanueva
  Formal Verification of Web Sites
  3rd Int'l Workshop on Automated Specification and Verification of Web Systems WWV'07
  Electronic Notes in Theoretical Computer Science, 200(3) :103-118, May 2008.
  © Elsevier Science
  Available: Abstract / PDF

• C. Fuhs, R. Navarro-Marset, C. Otto, J. Giesl, S. Lucas, and P. Schneider-Kamp
Search Techniques for Rational Polynomial Orders
9th International Conference on Artificial Intelligence and Symbolic Computation, AISC'08
LNAI to appear, 2008.
© Springer-Verlag
Available: Abstract / PDF

• R. Gutierrez, S. Lucas, and X. Urbain
Usable Rules for Context-Sensitive Rewrite Systems
19th International Conference on Rewriting Techniques and Applications, RTA'08
LNCS 5117:128-141, 2008.
© Springer-Verlag
Available: Abstract / PDF

• M. Katelman, S. Escobar, J. Meseguer.
  Directed-Logical Testing for Functional Verification of Microprocessors
  In proceedings of 6th ACM-IEEE Int'l Conf. on Formal Methods and Models for Codesign (MEMOCODE'2008),
  ACM Press to appear, 2008
  © ACM Press
  

• S. Lucas and J. Meseguer
  Operational Termination of Membership Equational Programs: the Order-Sorted Way
  7th International Workshop on Rewriting Logic and its Applications, WRLA'08
  Electronic Notes in Theoretical Computer Science, to appear, 2008.
  © Elsevier Science
  Available: Abstract / PDF

• S. Lucas and J. Meseguer
  Order-Sorted Dependency Pairs
  10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP'08
  ACM Press, to appear, 2008.
  © ACM Press
  Available: Abstract / PDF

• S. Lucas and J. Meseguer
  Termination of Just/Fair Computations in Term Rewriting
  Information and Computation 206(5) :652-675, May 2008.
  Elsevier Science
  Available: Abstract / PDF

• S. Lucas and R. Navarro-Marset
  Comparing CSP and SAT solvers for polynomial constraints in termination provers
  Selected papers of the 7th Spanish Conference on Programming and Computer Languages, PROLE'07
  Electronic Notes in Theoretical Computer Science, 206:75-90, April 2008. 2008.
  Elsevier Science
  Available: Abstract / PDF

2007

• B. Alarcon, R. Gutierrez, J. Iborra, and S. Lucas
Proving Termination of Context-Sensitive Rewriting With MU-TERM
Electronic Notes in Theoretical Computer Science, 188:105-115, 2007.
© Elsevier Science
Available: Abstract / PDF

• B. Alarcon, R. Gutierrez, and S. Lucas
Improving the context-sensitive dependency graph
Electronic Notes in Theoretical Computer Science, 188:91-103, 2007.
© Elsevier Science
Available: Abstract / PDF

• B. Alarcon and S. Lucas
Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs
6th International Symposium on Frontiers of Combining Systems, FroCoS'07
LNCS 4720:73-87, 2007.
© Springer-Verlag
Available: Abstract / PDF

• M. Alpuente, D. Ballis, M. Falaschi, P. Ojeda and D. D. Romero
  A Fast Algebraic Web Verification Service
  First Int'l Conf. on Web Reasoning and Rule Systems RR 2007
  Innsbruck, Austria, June 7-8, 2007
  LNCS 4524: 239-248, 2007.
  Extended and revised version of this paper
  © Springer-Verlag
  Available: Abstract / PDF
  
  
• M. Alpuente, S. Escobar, and M. Falaschi (Eds.)
Automated Specification and Verification of Web Systems, 2nd Int'l Workshop
© IEEE Computer Society Press, 2007
Available: IEEE Xplore link

• M. Alpuente. S. Escobar, and S. Lucas
Removing Redundant Arguments Automatically
(This article is an extended version of this paper)
Theory and Practice of Logic Programming 7(1&2):3-35, 2007.
Extended and revised version of this paper
© Cambridge University Press
Available: DOI link PDF (CORR version)


• M. Alpuente. B. Gramlich, and A. Villanueva
  
A framework for Timed Concurrent Constraint Programming with External Functions
Electronic Notes in Theoretical Computer Science, 188C: 143-155, 2007
© Elsevier
Available: PDF

• M. Clavel, F. Duran, S. Lucas, J. Meseguer, and P. Olveczky
  The Maude Formal Tool Environment
  Proc. of CALCO tools 2007,
  Bergen, Norway, August 20, 2007
  LNCS 4624:173-178, Springer-Verlag, Berlin, 2007.
  © Springer-Verlag
  Available: Abstract

• S. Escobar, J. Meseguer
  Symbolic Model Checking of Infinite-State Systems Using Narrowing
  In proceedings of 18th International Conference on Rewriting Techniques and Applications (RTA 2007),
  LNCS volume 4533, pages 153-168, 2007.
  © Springer-Verlag
  Available: PDF

• S. Escobar, C. Meadows, J. Meseguer.
  Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer
  In proceedings of 1st International Workshop on Security and Rewriting Techniques (SecReT 2006),
  Electronic Notes in Theoretical Computer Science, volume 171, pages 23-36, 2007.
  © Elsevier
  Available: DOI link PDF

• M.M. Gallardo, C. Joubert, P. Merino, and D. Sanan
  C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs
  Proceedings of the 14th International SPIN Workshop on Model Checking of Software
  SPIN'07 (Berlin, Germany), Jul 2007.
  LNCS 4595, To appear.
  © Springer-Verlag
  Available: Abstract / PDF / Appendix / BibTeX entry

• M.M. Gallardo, C. Joubert, P. Merino, and D. Sanan
  On-the-Fly Model Checking for C Programs with Extended CADP in FMICS-jETI
  Proceedings of the 12th IEEE International Conference on Engineering of Complex Computer Systems
  ICECCS'07 (Auckland, New Zealand), Jul 2007.
  © IEEE Computer Society Press
  Available: Abstract / PDF / BibTeX entry

• M.M. Gallardo, C. Joubert, and P. Merino
  On-the-Fly Data Flow Analysis based on Verification Technology.
  Proceedings of the 6th International Workshop on Compiler Optimization meets Compiler Verification COCV'2007 (Braga, Portugal), Mar 2007.
  ENTCS, To appear.
  © Elsevier
  Available: Abstract / PDF / BibTeX entry

• S. Lucas
  Practical use of polynomials over the reals in proofs of termination
  In Proc. of 9th International Conference on Principles and Practice of Declarative Programming, PPDP'07
  pages 39-50, ACM Press, 2007
  © ACM Press
  Available: Abstract

2006

• B. Alarcon, R. Gutierrez, and S. Lucas
Context-Sensitive Dependency Pairs
26th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'06
LNCS 4337:297-308, Springer-Verlag, Berlin, 2006.
© Springer-Verlag
Available: Abstract / PDF

• B. Alarcon and S. Lucas.
  Building .NET GUIs for Haskell applications
4th International Conference on .NET Technologies,
University of West-Bohemia, pages 57-66, 2006.
Available: Abstract / PDF
• M. Alpuente, D. Ballis, and M. Falaschi
Rule-based Verification of Web Sites
Software Tools for Technology Transfer, 8(6):565-585, 2006.
Extended and revised version of this paper
© Springer-Verlag
Available: Abstract / PDF


• M. Alpuente, D. Ballis, M. Falaschi, and D. Romero
A Semi-automatic Methodology for Repairing Faulty Web Sites
4th IEEE Int'l Conf on Software Engineering and Formal Methods SEFM, pages 31-40, 2006.
© IEEE Computer Society Press
Available: Abstract / PDF

• M. Alpuente, S. Escobar, M. Falasch (Eds.)
  Automated Specification and Verification of Web Sites, 1st Int'l Workshop,
  Electronic Notes in Theoretical Computer Science Volume 157, Issue 2 (212 pages), 22 May 2006
  © Elsevier Science, North-Holland
  Available: WWV'05 pre-proceedings
  
• M. Alpuente, M. M. Gallardo, E. Pimentel, A. Villanueva
  Verifying Real-Time Properties of tccp programs
  Journal of Universal Computer Science, Vol.12, No. 11, pp. 1551 - 1573, 2006
  © Springer-Verlag
  Available: Abstract / PDF
  
  
• M. Alpuente, B. Gramlich and  A. Villanueva
Timed Concurrent Constraint Programming with Instantaneous Computations
In Proc. VI Jornadas sobre Programacion y Lenguajes, PROLE'06.

• D. Ballis, and D. Romero
Fixing Web Sites Using Correction Strategies
2nd Int'l Workshop on Automated Specification and Verification of Web Sites, WWV'06, pages 495-502.
Paphos, Cyprus. 2006
© IEEE Computer Society, to appear.
Available: Abstract / PDF


• D. Ballis, and D. Romero
Filtering of XML Documents
2nd Int'l Workshop on Automated Specification and Verification of Web Sites, WWV'06, pages 503-509.
Paphos, Cyprus. 2006
© IEEE Computer Society, to appear.
Available: Abstract / PDF
• S. Escobar, J. Meseguer, P. Thati.
  Narrowing and Rewriting Logic: from Foundations to Applications (invited paper)
  In proceedings of 15th Int'l Workshop on Functional and (Constraint) Logic Programming (WFLP'06),
  ENTCS to appear, 2006.
  © Elsevier
  
• S. Escobar, C. Meadows, J. Meseguer.
  A Rewriting-Based Inference System for the NRL Protocol Analyzer and its Meta-Logical Properties
  Theoretical Computer Science, Volume 367, Issues 1-2 , 24 November 2006, Pages 162-202.
  Extended and revised version of this paper.
  © Elsevier
  Available: DOI link Preliminary version
• S. Escobar, C. Meadows, J. Meseguer.
  Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer
  In proceedings of 1st International Workshop on Security and Rewriting Techniques (SecReT 2006), To appear 2006.
  © Elsevier
  
• B. Gramlich and S. Lucas
  Generalizing Newman's Lemma for Left-Linear Rewrite Systems
  Proc. of 17th International Conference on Rewriting Techniques and Applications, RTA'06,
  LNCS 4098:66-80, Springer-Verlag, Berlin, 2006.
  © Springer-Verlag
  Available: Abstract / PDF
• S. Lucas
  Proving Termination of Context-Sensitive Rewriting by Transformation
  Information and Computation, 204(12):1782-1846, 2006.
  © Elsevier
  Available: Abstract
• S. Lucas
  On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
  Applicable Algebra in Engineering, Communications and Computing, 17(1):49-73, 2006.
  © Springer-Verlag
  Available: Abstract PDF (preprint)
• S. Lucas
  Rewriting-Based Navigation of Web Sites: Looking for Models and Logics
  1st International Workshop on Automated Specification and Verification of Web Sites, WWV'05
Electronic Notes in Theoretical Computer Science, 157(2):79-85, 2006.
© Elsevier
Available: Abstract

2005

• M. Alpuente, D. Ballis, and M. Falaschi
  A Rewriting-based Framework for Web sites Verification
  5th Int'l Workshop on Rule-based Programming RULE 2004,
  Aachen (Germany).
  ENTCS 124(1):41-61, 2005.
  © Elsevier Science, North-Holland
  Available: Abstract / PDF
  
  
• María Alpuente, Santiago Escobar, Salvador Lucas.
  A Note on Syntactic Annotations for Narrowing
  In proceedings of Quintas Jornadas sobre Programación y Lenguajes, PROLE'05, 2005.
  © Thomson
  Available: Abstract PDF
  
  
• M. Alpuente, M. Falaschi, and A. Villanueva.
A Symbolic Model Checker for tccp Programs
13th ERCIM Int'l Workshop on Rapid Integration of Software Engineering Techniques
RISE 2004, Luxembourg (LU)
LNCS 3475:45-56, 2005
© Springer-Verlag
Available: Abstract / PDF / PostScript


• M. Alpuente, M. M. Gallardo, E. Pimentel, and A. Villanueva.
  A Semantic Framework for the Abstract Model Checking of tccp programs
  Theoretical Computer Science, 346(1):58-95, 2005. 
  Extended and revised version of this paper
  © ElsevierScience, North-Holland
  Available: Abstract / PDF / PostScript
  

• M. Alpuente, S. Escobar, and S. Lucas.
  A Note on Syntactic Annotations for Narrowing
  © Thomson
  V Jornadas sobre Programacion y Lenguajes, PROLE'05, pages 25-30, 2005.
  Available: Abstract
  
  

  M. Alpuente, Mari­a del Mar Gallardo, Ernesto Pimentel and A. Vilanueva.
  Semantic Framework for the Abstract Model Checking of tccp programs (Extended Abstract)
  © Thomson
  In Proc. V Jornadas sobre Programacion y Lenguajes, PROLE'05, pages 97-100, 2005.
  Available: Abstract PostScript PDF BibTeX Entry
  
  

  M. Alpuente, Mari­a del Mar Gallardo, Ernesto Pimentel and A. Vilanueva.
  Verifying Real-Time Properties of tccp Programs
  © Thomson
  V Jornadas sobre Programacion y Lenguajes, PROLE'05, pages 85-94, 2005.
  Available: Abstract PostScript PDF BibTeX Entry
  
  

  M. Alpuente, M. Falaschi, and A. Villanueva. A Symbolic Model Checker for tccp Programs
  13th ERCIM Int'l Workshop on Rapid Integration of Software Engineering Techniques,
  RISE 2004, Luxembourg (LU), 2004.
  LNCS 3475:45-56, 2005
  © Springer-Verlag
  Available: Abstract / PDF / PostScript

• M. Alpuente, M. Hanus, S. Lucas, and G. Vidal
  Specialization of Functional Logic Programs Based on Needed Narrowing
  Theory and Practice of Logic Programming 5(3):273-303, 2005.
  Extended and revised version of this paper
  © Cambridge University Press
  Available: Abstract / Online article (with proofs) / BibTeX entry
  
  
• M. Alpuente, S. Lucas
  Connecting Remote Tools: Do it by yourSELF!
  ERCIM News 61, April 2005
  Available: Online article


• F. Duran, S. Escobar, and S. Lucas.
  On-demand evaluation for Maude
  In Proc. of Rule-Based Programming, RULE'04,
  Electronic Notes in Theoretical Computer Science, 124(1):25-39, 2005.
  © Elsevier
  Available: Abstract PDF PostScriptBibTeX entry
  
  
• F. Duran, S. Escobar, and S. Lucas.
  New evaluation commands for Maude within Full Maude
  In Proc. of 5th International Workshop on Rewriting Logic and Applications, WRLA'04,
  Electronic Notes in Theoretical Computer Science, 117:263-284, 2005.
  © Elsevier
  Available: Abstract PDF PostScriptBibTeX entry

• S. Escobar, C. Meadows, J. Meseguer.
  A Rewriting-Based Inference System for the NRL Protocol Analyzer: Grammar Generation
  In proceedings of 3rd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code,
  pages 1-12, 2005.
  © ACM Press
  Available: ACM link PDF
• S. Escobar, J. Meseguer, and P. Thati.
  Natural Narrowing for General Term Rewriting Systems
  16th Int'l Conf. on Rewriting Techniques and Applications RTA 2005, Nara (Japan).
  LNCS 3467:279-293, 2005.
  © Springer-Verlag
  Available: PDF
  
• S. Escobar, J. Meseguer, and P. Thati.
  Natural Rewriting for General Term Rewriting Systems
  Int'l Symp. on Logic Based Program Synthesis and Tranformation
  LOPSTR 2004, Verona (Italy).
  LNCS 3573:101-116, 2005.
  © Springer-Verlag
  Available: PDF
  
• V. Estruch, C. Ferri, J. Hernandez-Orallo, M.J. Ramirez-Quintana,
  Distance Based Generalisation
  Best Student Paper
  15th International Conference on Inductive Logic Programming
  LNCS 3625:87-102, 2005
  
• V. Estruch, C. Ferri, J. Hernandez-Orallo, M.J. Ramirez-Quintana,
  Web Categorisation Using Distance-Based Decision Trees
  1st International Workshop on Automated Specification and Verification of Web Sites, WWV'05
Electr. Notes Theor. Comput. Sci. 157(2): 35-40 (2006)
© Elsevier Science, North-Holland

• M. Falaschi and A. Villanueva
  Automatic Verification of Timed Concurrent Constraint Programs
  Theory and Practice of Logic Programming, 2005. To appear
  © Cambridge University Press
  Available: Abstract / PDF / PostScript / BibTeX entry


• B. Gramlich and S. Lucas (editors)
  Reduction Strategies in Rewriting and Programming (special issue)
  Journal of Symbolic Computation, volume 40, issue 1, July 2005.
  © Elsevier
  Available:Summary


• S. Lucas (editor)
  Fourth Spanish Conference on Programming and Computer Languages, PROLE 2004 - Selected papers
  Electronic Notes in Theoretical Computer Science, volume 137, issue 1, 2005.
  © Elsevier
  Available:
• S. Lucas
  Polynomials over the reals in proofs of termination: from theory to practice
  RAIRO Theoretical Informatics and Applications, 39(3):547-586, 2005.
  © EDP Sciences
  Available: Abstract / PDF (preprint)
• S. Lucas
  
Strategies in Programming Languages Today
Final proceedings of the 4th International Workshop on Reduction Strategies in Rewriting and Programming, WRS'04
Electronic Notes in Theoretical Computer Science, 124(2):113-118, 2005.
© Elsevier
Available: Abstract / PDF
• S. Lucas, C. Marché, and J. Meseguer
  Operational Termination of Conditional Term Rewriting Systems
  Information Processing Letters, 95(4):446-453, 2005.
  © Elsevier
  Available: Abstract / PDF (preprint)
• S. Lucas and J. Meseguer
  Termination of Fair Computations in Term Rewriting
  12th International Conference on Logic for Programming, Artificial intelligence and Reasoning, LPAR'05,
  © Springer-Verlag
  LNCS 3835:184-198, Springer-Verlag, Berlin, 2005.
  Available: Abstract / PDF (preprint)