herranz_latin1.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob herranz_latin1.bib -c 'author : "Herranz"' publications_latin1.bib}}
@inproceedings{fdez-soriano11:_tool_integ_const_logic_progr_spread,
  tipoactividad = {Ponencias en congresos},
  internacional = {no},
  author = {Ana María {Fernández-Soriano} and Julio Mariño and {Ángel} Herranz},
  title = {A Tool for the Integration of Constraint Logic Programming in Spreadsheets},
  booktitle = {Actas XI Jornadas sobre Programación y Lenguajes},
  pages = {243-252},
  year = 2011,
  editor = {{Purificación} Arenas and {Víctor M.} Gulías and Pablo Nogueira},
  address = {A Coruña, Spain},
  month = sep,
  note = {ISBN 978-84-9749-487-8}
}
@inproceedings{herranz11:_verif_implem_prior_monit_java,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  author = {{Ángel} Herranz and Julio Mariño},
  title = {A Verified Implementation of Priority Monitors in {Java}},
  booktitle = {Papers presented at the 2nd. International Conference on Formal Verification of Object-Oriented Software (FoVeOOS'11},
  pages = {244-259},
  year = 2011,
  editor = {Bernhard Beckert and Ferruccio Damiani and Dilian Gurov},
  number = 26,
  address = {Turin, Italy},
  publisher = {Karlsruhe Reports in Informatics},
  note = {ISSN 2190-4782}
}
@inproceedings{2011:hema:slpoofs,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  author = {{Ángel} Herranz and Julio Mariño},
  title = {Synthesis of Logic Programs from Object-Oriented Formal Specifications},
  booktitle = {Technical Communications of the 27th International Conference
               on Logic Programming},
  month = jul,
  year = 2011,
  pages = {95-105},
  ee = {http://dx.doi.org/10.4230/LIPIcs.ICLP.2011.95},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  volume = {11},
  isbn = {978-3-939897-31-6},
  note = {ISBN: 978-3-939897-31-6},
  address = {Lexington, Kentucky, USA}
}
@inproceedings{2011:hebemama:mvernp,
  author = {{Ángel} Herranz and Clara Benac and Guillem Marpons and Julio Mariño},
  title = {Mechanising the Validation of {ERTMS} Requirements and New Procedures},
  booktitle = {9th World Congress on Railway Research},
  pages = {33},
  year = {2011},
  month = may,
  pdf = {http://babel.ls.fi.upm.es/~angel/papers/H05_Herranz_Angel.pdf}
}
@techreport{2010:pehe:ezweb_comm_models,
  author = {{Ángel} Herranz and {Iván} {Pérez}},
  title = {Communication Models for Resource Mashups},
  institution = {Babel Group, Universidad Politécnica de Madrid},
  year = {2010},
  number = {UPM-BABEL-2010-002},
  month = mar
}
@techreport{2010:pehe:ezweb_types,
  author = {{Ángel} Herranz and {Iván} {Pérez}},
  title = {Compatible Communication in Mashups},
  institution = {Babel Group, Universidad Politécnica de Madrid},
  year = {2010},
  number = {UPM-BABEL-2010-001},
  month = jan
}
@phdthesis{aherranz:thesis,
  author = {{Ángel} Herranz},
  title = {An Object-Oriented Formal Notation: Executable Specifications in Clay},
  school = {Universidad Politécnica de Madrid},
  year = {2011},
  month = jan
}
@inproceedings{hema:2010:esoofn,
  author = {{Ángel} Herranz and Julio Mariño},
  title = {Executable Specifications in an Object Oriented Formal Notation},
  booktitle = {20th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2010},
  organization = {Research Institute for Symbolic Computation (RISC) of the Johannes Kepler University Linz},
  address = {Hagenberg, Austria},
  month = jul,
  year = {2010},
  abstract = {Early validation of requirements is crucial for the rigorous
                  development of software. Without it, even the most formal of the
                  methodologies will produce the wrong outcome. 
                  One successful approach, popularised by some of the so-called
                  lightweight formal methods, consists in generating (finite,
                  small) models of the specifications. Another possibility is to build a
                  running prototype from those specifications.
                  In this paper we show how to obtain executable prototypes from formal
                  specifications written in an object oriented notation by translating
                  them into logic programs. 
                  This has a number of advantages over other lightweight methodologies.
                  For instance, we recover the possibility of dealing with recursive
                  data types as specifications that use them often lack finite models.},
  pages = {144-158},
  tipoactividad = {Ponencias en congresos},
  international = {yes},
  revisores = {yes},
  pdf = {http://babel.ls.fi.upm.es/~angel/papers/clay2prolog-LOPSTR2010preproceedings.pdf}
}
@article{DBLP:journals_entcs_Marpons-UceroMCHFMP09,
  author = {Guillem Marpons and Julio Mariño and Manuel Carro and
                  {Ángel} Herranz and Lars-{\AA}ke Fredlund and
                  {Juan José {Moreno-Navarro}} and {Álvaro} Polo},
  title = {A Coding Rule Conformance Checker Integrated into {GCC}},
  journal = {ENTCS},
  volume = 248,
  year = 2009,
  month = {August 5},
  pages = {149-159},
  url = {http://dx.doi.org/10.1016/j.entcs.2009.07.065},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  tipoactividad = {Artículos en revistas},
  internacional = {yes},
  abstract = {Coding rules are often used in industry to foster best
                  practices when coding software and to avoid the many
                  hazardous constructions present in languages such as
                  C or C++. Predictable, reliable tools are needed to
                  automatically measure adherence to these practices,
                  as manually checking for compliance is
                  cumbersome. Moreover, due to the wide range of
                  possible coding rule sets, easy of customization is
                  a need in order for these tools to be of practical
                  use. With this aim in mind, we present an extension
                  of the GNU Compiler Collection (GCC) that flags
                  those code fragments that do not conform to coding
                  rules belonging to a given set. These sets of coding
                  rules can be defined using a high-level declarative
                  language based on logic programming, thereby making
                  it possible to easily check code for conformance
                  with respect to rules addressing the particular
                  needs of a project, company, or application area.},
  issn = {1571-0661}
}
@inproceedings{hemacamo:2009:mcssr,
  author = {{Ángel} Herranz and
               Julio Mariño and
               Manuel Carro and
               Juan José {Moreno-Navarro}},
  title = {Modeling Concurrent Systems with Shared Resources},
  booktitle = {Formal Methods for Industrial Critical Systems, 14th International
               Workshop, FMICS 2009, Eindhoven, The Netherlands,
                  November 2-3, 2009. Proceedings},
  pages = {102-116},
  series = {Lecture Notes in Computer Science},
  volume = {5825},
  year = {2009},
  isbn = {978-3-642-04569-1},
  issn = {0302-9743},
  url = {http://www.springerlink.com/content/b83m037648436667/},
  pdf = {http://www.springerlink.com/content/b83m037648436667/fulltext.pdf},
  abstract = {Testing is the more widely used approach to (partial)
                  system validation in industry. The introduction of
                  concurrency makes exhaustive testing extremely
                  costly or just impossible, requiring shifting to
                  formal verification techniques. We propose a
                  methodology to design and verify a concurrent system
                  that splits the verification problem in two
                  independent tasks: internal verification of shared
                  resources, where some concurrency aspects like
                  mutual exclusion and conditional synchronisation are
                  isolated, and external verification of processes,
                  where synchronisation mechanisms are not
                  relevant. Our method is language independent,
                  non-intrusive for the development process, and
                  improves the portability of the resulting system. We
                  demonstrate it by actually checking several
                  properties of an example application using the TLC
                  model checker.}
}
@inproceedings{marpons08:_codin_rule_confor_check_integ_into_gcc,
  tipoactividad = {Ponencias en congresos},
  internacional = {no},
  revisores = {yes},
  author = {Guillem Marpons and Julio Mariño and Manuel Carro and {Ángel}
                  Herranz and Lars-{\AA}ke Fredlund and Juan José
                  {Moreno-Navarro} and {Álvaro} Polo},
  title = {A Coding Rule Conformance Checker Integrated into {GCC}},
  abstract = { Coding rules are often used in industry for codifying
                  software best practices and avoiding the many hazardous
                  constructions present in languages such as C or
                  C++. Predictable and customisable tools are needed to
                  automatically measure adherence to these practices.  Many of
                  the properties about software needed for rule conformance
                  analysis are calculated by modern compilers.  We present an
                  extension of the GNU Compiler Collection (GCC) that flags
                  those code fragments that do not conform to a given set of
                  rules. The user can define coding rules using a high-level
                  declarative language based on logic programming.  },
  booktitle = {VIII Jornadas sobre Programación y Lenguajes, {PROLE} 2008},
  pages = {245--249},
  address = {Gijón, Spain},
  editor = {Jesús M. {Almendros Jiménez} and María José {Suárez-Cabal}},
  month = {October 7--10},
  year = 2008,
  isbn = {978-84-612-5819-2},
  pdf = {http://babel.ls.fi.upm.es/~gmarpons/pubs/PROLE08Codingrules.pdf}
}
@inproceedings{marpons08:_autom_codin_rule_confor_check,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  revisores = {yes},
  title = {Automatic Coding Rule Conformance Checking Using Logic
                  Programming},
  author = {Guillem Marpons and Julio {Mari{\~n}o-Carballo} and Manuel
                  Carro and {Ángel} Herranz and Juan Jos{\'e} {Moreno-Navarro}
                  and Lars-{\AA}ke Fredlund},
  abstract = {An extended practice in the realm of Software Engineering
                  and programming in industry is the application of
                  \emph{coding rules}. Coding rules are customarily used to
                  constrain the use (or abuse) of certain programming language
                  constructions.  However, these rules are usually written
                  using natural language, which is intrinsically ambiguous and
                  which may complicate their use and hinder their automatic
                  enforcement.  This paper presents some early work aiming at
                  defining a framework to formalise and check for coding rule
                  conformance using logic programming.  We show how a certain
                  class of rules -- \emph{structural} rules -- can be
                  reformulated as logic programs, which provides both a
                  framework for formal specification and also for automatic
                  conformance checking using a Prolog engine.  Some examples
                  of rules belonging to actual, third-party coding rule sets
                  are discussed, along with the corresponding Prolog code.
                  Experimental data regarding the practicality and impact of
                  their application to real-life software projects is
                  presented and discussed.  },
  booktitle = {Practical Aspects of Declarative Languages, 10th
                  International Symposium, {PADL} 2008},
  publisher = {Springer},
  year = 2008,
  month = {January 7--8},
  address = {San Francisco {CA}, {USA}},
  volume = 4902,
  editor = {Paul Hudak and David Scott Warren},
  isbn = {978-3-540-77441-9},
  pages = {18--34},
  series = {Lecture Notes in Computer Science},
  url = {http://dx.doi.org/10.1007/978-3-540-77442-6_3}
}
@inproceedings{pehemumo:2008:mmr,
  tipoactividad = {Ponencias en congresos},
  internacional = {no},
  revisores = {yes},
  author = {Iván Pérez and {Ángel} Herranz and Susana Muñoz and Juan José
                  {Moreno-Navarro}},
  title = {Modelling Mash-Up Resources},
  booktitle = {13th Conference on Software Engineering and
                  Databases, JISBD'08},
  descripcion = {Modelo formal para representar mash-ups y los
                  componentes que lo forman. El modelo formal se
                  ofrece en axiomas de la lógica descriptiva a través
                  de una ontología.},
  pages = {135-146},
  address = {Gijón, Spain},
  month = {October 7--10},
  year = 2008,
  isbn = {978-84-612-5820-8},
  pdf = {http://babel.ls.fi.upm.es/~angel/papers/2008jisbd-finalcopy.pdf}
}
@techreport{xmc:2007:_study_of_exist_codin_rule,
  tipoactividad = {Otras publicaciones},
  internacional = {yes},
  author = {Julio Mariño and {Ángel} Herranz and Lars-{\AA}ke Fredlund and
                  Manuel Carro and V{\'i}ctor {Pablos-Ceruelo} and Guillem Marpons and Juan
                  José {Moreno-Navarro}},
  title = {Study of existing coding rule formalisms and compendium of
                  common hazards.  {U}se of Coding Rules in Software Industry},
  descripcion = {Estudio de los formalismos existentes para reglas de
                  codificación, relación de riesgos de software más comunes y
                  resultados de encuesta a socios del proyecto {GlobalGCC}.},
  institution = {Facultad de Informática, Universidad Politécnica de Madrid},
  year = 2007,
  address = {Boadilla del Monte, Madrid, Spain},
  month = nov,
  annote = {Deliverable for the {GlobalGCC} Project}
}
@inproceedings{marpons:2007:wlpe,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  author = {Guillem Marpons and Julio Mari{\~n}o and {Ángel}
                  Herranz and Lars-{\AA}ke Fredlund and Manuel Carro and Juan
                  Jos{\'e} {Moreno-Navarro}},
  title = {Automatic Coding Rule Conformance Checking Using Logic
                  Programs},
  abstract = { Coding rules are customarily used to constrain the use (or
                  abuse) of certain constructions in a programming language.
                  Standard coding rule sets exist that target different
                  languages and application domains.  However, these rules are
                  usually written using a natural language, which is
                  intrinsically ambiguous, and which may hinder their
                  automatic application.  This short paper presents some early
                  work aiming at defining a framework to formalise and check
                  for coding rule conformance using logic programming.  We
                  show how a certain class of rules -- \emph{structural} rules
                  -- can be reformulated as logic programs.  Some real
                  examples, including Prolog code formalising them, are shown
                  and discussed.  },
  revisores = {yes},
  booktitle = {17th Workshop on Logic-based methods in Programming
                  Environments, {WLPE} 2007},
  pages = 47,
  url = {http://arxiv.org/abs/0711.0344},
  year = 2007,
  editor = {Patricia Hill and Vim Vanhoof},
  address = {Porto, Portugal},
  month = sep
}
@article{marpons:2007:corr,
  author = {Guillem Marpons and Julio Mari{\~n}o and {Ángel}
                  Herranz and Lars-{\AA}ke Fredlund and Manuel Carro and Juan
                  Jos{\'e} {Moreno-Navarro}},
  abstract = { Coding rules are customarily used to constrain the use (or
                  abuse) of certain constructions in a programming language.
                  Standard coding rule sets exist that target different
                  languages and application domains.  However, these rules are
                  usually written using a natural language, which is
                  intrinsically ambiguous, and which may hinder their
                  automatic application.  This short paper presents some early
                  work aiming at defining a framework to formalise and check
                  for coding rule conformance using logic programming.  We
                  show how a certain class of rules -- \emph{structural} rules
                  -- can be reformulated as logic programs.  Some real
                  examples, including Prolog code formalising them, are shown
                  and discussed.  },
  title = {Automatic Coding Rule Conformance Checking Using Logic
                  Programs},
  journal = {CoRR},
  volume = {abs/0711.0344},
  year = 2007,
  month = nov,
  url = {http://arxiv.org/abs/0711.0344},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@misc{marpons:2007:sas,
  tipoactividad = {Otras publicaciones},
  internacional = {yes},
  abstract = { This short paper presents some early work in the context of
                  an European project aiming at defining a framework to
                  formalise and check for coding rule conformance using logic
                  programming.  We show how a certain class of rules --
                  \emph{structural} rules -- can be reformulated as logic
                  programs. This provides both a framework for formal
                  specification and also for automatic conformance checking
                  using a Prolog engine.  },
  revisores = {yes},
  author = {Guillem Marpons and Julio Mariño and {Ángel} Herranz and
                  Lars-{\AA}ke Fredlund and Manuel Carro and Juan José
                  {Moreno-Navarro}},
  title = {Towards Checking Coding Rule Conformance Using Logic
                  Programming},
  month = aug,
  year = 2007,
  note = {Poster at the 14th International Static Analysis
                  Symposium, SAS 2007},
  address = {Kongens Lyngby, Denmark},
  pdf = {http://babel.ls.fi.upm.es/~gmarpons/pubs/SAS07CodingrulesPoster.pdf}
}
@article{tahemo:2009:srvdpftutmc,
  author = {Toufik Taibi and {Ángel} Herranz and Juan José
                  {Moreno-Navarro}},
  title = {Stepwise Refinement Validation of Design Patterns Formalized
                  in TLA+ Using the TLC Model Checker},
  journal = {Journal of Object Technology (JOT, \url{http://www.jot.fm/general/about/})},
  year = {2009},
  volume = {8},
  number = {2},
  month = mar,
  issn = {1660-1769},
  pages = {137-161},
  doi = {doi:10.5381/jot.2009.8.2.a3},
  pdf = {http://www.jot.fm/issues/issue_2009_03/article3.pdf},
  abstract = {Despite being around for only a little more than a
                  decade, design patterns have proved to be successful
                  reuse artifacts. However, the fact that they are
                  mostly described informally gives rise to ambiguity
                  and hinders correct usage. This paper discusses how
                  to formally specify the "solution element" of
                  patterns using TLA+, the formal specification
                  language of Temporal Logic of Actions (TLA). The
                  focus is first on formally specifying the most
                  abstract version of a pattern before validly doing
                  stepwise refinements by adding more details along
                  the way until reaching a concrete
                  implementation. Checking that the refinement
                  properties hold was done using TLC (the TLA+ model
                  checker).},
  tipoactividad = {Artículos en revistas},
  internacional = {yes}
}
@inbook{hemo:2007:mrdps,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Design Pattern Formalization Techniques},
  chapter = {Modeling and Reasoning about Design Patterns in
                  {SLAM-SL}},
  publisher = {IGI Publishing},
  year = {2007},
  month = mar,
  isbn = {978-1-59904-219-0},
  note = {Other ISBN: 978-1-59904-221-3},
  abstract = {The main main subject of the chapter is how design
                  patterns can be described as class
                  operations. Additionally, we describe two possible
                  applications: how to reason about design patterns,
                  and how a design can be automatically refactored
                  using design patterns.},
  tipoactividad = {Capítulos de libro},
  internacional = {yes},
  description = {El principal objetivo del capítulo es el estudio de
                  la descripción de patrones de diseño como operadores
                  matemáticos sobre clases. Además, se describen dos
                  posibles aplicaciones de la formalización:
                  razonamiento sobre patrones de diseño y la
                  refactorización automática de los diseños utilizando
                  los operadores de clases definidos.},
  pdf = {http://babel.ls.fi.upm.es/~angel/papers/taibichapter-finalcopy.pdf}
}
@article{hema:2004:cupcam2003-otraruta,
  author = {{Ángel} Herranz and Julio Mariño},
  title = {Por otra ruta, por favor (CUPCAM 2003, problema E,
                  solución)},
  journal = {Novatica},
  year = {2004},
  volume = {1},
  number = {170},
  pages = {73},
  month = jul,
  note = {Sección ``Programar es crear''},
  url = {http://www.ati.es/novatica/2004/170/170-73.pdf}
}
@article{lehe:2004:cupcam2003-refactor,
  author = {José A. Leiva and {Ángel} Herranz},
  title = {Un refactorizador simple (CUPCAM 2003, problema D,
                  solución)},
  journal = {Novatica},
  year = {2004},
  volume = {1},
  number = {169},
  pages = {74},
  month = may,
  note = {Sección ``Programar es crear''},
  url = {http://www.ati.es/novatica/2004/169/169-74.pdf}
}
@article{cahemasa:2002:icpc-final2001-aeropuerto,
  author = {Manuel Carro and {Ángel} Herranz and Julio Mariño and Pablo
                  Sánchez},
  title = {Configuración de un aeropuerto: solución},
  journal = {Novatica},
  year = {2002},
  volume = {1},
  number = {156},
  pages = {72},
  month = mar,
  note = {Sección ``Programar es crear''},
  url = {http://www.ati.es/novatica/2002/156/156-72.pdf}
}
@article{hemacasa:2002:icpc-final2001-bosque,
  author = {{Ángel} Herranz and Julio Mariño and Manuel Carro and Pablo
                  Sanchez},
  title = {No taléis el bosque por culpa de los árboles: solución},
  journal = {Novatica},
  year = {2002},
  volume = {1},
  number = {159},
  pages = {74},
  month = sep,
  note = {Sección ``Programar es crear''},
  url = {http://www.ati.es/novatica/2002/159/159-74.pdf}
}
@article{hemacasa:2003:icpc-final2001-almejas,
  author = {{Ángel} Herranz and Julio Mariño and Manuel Carro and Pablo
                  Sanchez},
  title = {Almejas gigantes e interfaces de usuario (solución del
                  programa E)},
  journal = {Novatica},
  year = {2003},
  volume = {1},
  number = {161},
  pages = {70},
  month = jan,
  note = {Sección ``Programar es crear''},
  url = {http://www.ati.es/novatica/2003/161/161-70.pdf}
}
@article{grhema:2002:cc2001,
  author = {Carlos Gregorio and {Ángel} Herranz and Raquel Martinez},
  title = {Computing Curricula 2001},
  journal = {Novática},
  year = {2002},
  volume = {1},
  number = {157},
  pages = {47-54},
  month = may,
  abstract = { En diciembre de 2001 se publicó el informe final del
                  volumen \emph{Computer Science} del Computing Curricula
                  2001. Las recomendaciones desarrolladas por ACM y IEEE de
                  forma individual, tanto como las recomendaciones elaboradas
                  de forma conjunta, han sido y siguen siendo un punto de
                  referencia para todos los que nos dedicamos a la enseñanza
                  universitaria de la informática.  El objetivo de este
                  artículo es dar a conocer las líneas maestras del informe,
                  los principios del mismo, las nuevas áreas de conocimientos
                  y las diferentes estrategias de implementación sugeridas, el
                  objetivo final es que un lector interesado pueda hacerse una
                  idea clara de las propuestas fundamentales del informe.  },
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/cc2001.ps.gz},
  pdf = {http://www.ati.es/novatica/2002/157/157-47.pdf},
  note = {In Spanish}
}
@mastersthesis{aherranz:master,
  author = {{Ángel} Herranz},
  title = {Interpretación Abstracta de Lenguajes Lógico Funcionales},
  school = {Facultad de Informática, Universidad Politécnica de Madrid},
  year = {1993},
  address = {Campus de Montegancedo s/n, 28660, Boadilla del Monte,
                  Madrid, Spain},
  month = oct,
  note = {In Spanish},
  abstract = {The aim of this work is to formulate a framework for the
                  abstract interpretation of functional logic languages based
                  on its operational semantics that allows for the most usual
                  analyses needed in declarative programming: mode inference,
                  optimal garbage collection, detection of parallel
                  computations etc. Besides, it should allow for analyses of
                  particular features of a lazy language.  },
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/aherranz-master.ps.gz}
}
@article{mahemo:2007:dapp,
  tipoactividad = {Artículos en revistas},
  internacional = {yes},
  author = {Julio Mariño and {Ángel} Herranz and Juan José
                  {Moreno-Navarro}},
  title = {Demandedness Analysis with Partial Predicates},
  journal = {Theory and Practice of Logic Programming},
  issn = {1471-0684},
  year = 2007,
  volume = 7,
  number = {1-2},
  pages = {153-182},
  month = jan,
  descripcion = {El análisis de demanda pretende determinar en tiempo de
                  compilación qué cálculos van a ser realmente utilizados
                  durante la ejecución de un programa. Esta información puede
                  ser muy relevante para la implementación de lenguajes
                  lógico-funcionales.  Este trabajo propone un marco semántico
                  de predicados parciales, que podríamos ver como
                  realizaciones constructivas de ideales sobre un cierto
                  dominio. Con esto conseguimos dar una presentación concisa y
                  unificada de una familia de análisis de demanda,
                  relacionarlo con otras propuestas, ideas para su
                  implementación y, finalmente, demostrar la corrección de una
                  propuesta anterior basada en la resolución de ecuaciones de
                  demanda.}
}
@inproceedings{hemamo:2000:pp,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro} and Julio Mariño},
  title = {Demand Analysis with Partial Predicates},
  booktitle = {9th International Workshop on Functional and Logic
                  Programming (WFLP 2000)},
  year = {2000},
  month = sep,
  organization = {Universidad Politécnica de Valencia},
  address = {Benicassim, Spain}
}
@inproceedings{heno:2005:mtp,
  author = {{Ángel} Herranz and Pablo Nogueira},
  title = {More Than Parsing},
  booktitle = {Spanish Conference on Programming and Languages
                  ({CEDI-PROLE}'05)},
  pages = {193-202},
  year = 2005,
  editor = {Francisco Javier {López Fraguas}},
  month = {September},
  publisher = {Thomson Paraninfo},
  isbn = {84-9732-438-2},
  abstract = {We introduce \emph{Generalised Object Normal Form} (GONF), a
                  syntax formalism that enables language designers to define
                  concrete syntax in a form that \emph{also naturally} defines
                  the data structure of the abstract syntax tree. More
                  precisely, GONF's grammatical productions specify
                  \emph{simultaneously} and without annotations (1) concrete
                  syntax (a language and its parser) and (2) the collection of
                  \emph{language-independent} data type definitions
                  representing the abstract syntax tree accurately and
                  concisely.  These types can be materialised in languages
                  supporting inheritance or algebraic types, and preferably
                  parametric polymorphism. We also describe \emph{MTP}, an
                  available GONF-based tool.},
  url = {http://babel.ls.fi.upm.es/~angel/papers/finalcopy-2005prole.pdf}
}
@inproceedings{hemo:2003:fahme,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Formal Agility.  How Much of Each?},
  booktitle = {Taller de Metodologías Ágiles en el Desarrollo del
                  Software. VIII Jornadas de Ingeniería del Software y Bases
                  de Datos, JISBD 2003},
  pages = {47-51},
  year = {2003},
  month = nov,
  organization = {Grupo ISSI},
  address = {Alicante, España},
  abstract = { Agile Processes and Formal Methods (FM), water and oil,
                  impossible mixture?  Yes at first sight.  Nevertheless,
                  being formal methods weight processes and being agile
                  processes informal approaches to software development, it is
                  worth to study how much formal can be an agile process like
                  Extreme Programming (XP) and how much agile can be a formal
                  method.  On our view, some XP practices are suitable for a
                  formal approach.  },
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/finalcopy-jisbd2003.ps.gz}
}
@inproceedings{hemamo:2003:fesj,
  author = {{Ángel} Herranz and Noelia Maya and Juan José
                  {Moreno-Navarro}},
  title = {From Executable Specifications to Java},
  booktitle = {III Jornadas sobre Programación y Lenguajes, PROLE 2003},
  pages = {33-44},
  year = {2003},
  editor = {Juan José {Moreno-Navarro} and Manuel Palomar},
  address = {Alicante, España},
  month = nov,
  organization = {Departamento de Lenguajes y Sistemas Informáticos,
                  Universidad de Alicante},
  note = {Depósito Legal MU-2299-2003},
  abstract = { In this paper the authors study a pair of constructs in a
                  formal specification language that can be directly
                  translated into readable and relatively efficient code.
                  Those constructs are \emph{algebraic types} and (an extended
                  concept of logical) \emph{quantification}.  The translation
                  is guided by object oriented design patterns that makes the
                  synthesised code easily understandable by ordinary
                  developers.  Efficiency can be achieved thanks to the effort
                  of the user during the specification refinement process,
                  specification transformations and implementation issues of
                  the the design patterns.  },
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/finalcopy-prole2003.ps.gz}
}
@inproceedings{hemo:2003:slam-rad,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Rapid Prototyping and Incremental Evolution Using {SLAM}},
  booktitle = {14th IEEE International Workshop on Rapid System
                  Prototyping, RSP 2003)},
  pages = {},
  year = {2003},
  month = jun,
  address = {San Diego, California, USA},
  abstract = { The paper shows the outlines of the SLAM system, that
                  allows for an effective use of Formal Methods (FM) in Rapid
                  Application Development (RAD) and other prototyping
                  processes.  The SLAM system, includes an expressive object
                  oriented specification language and a development
                  environment that, among other features, is able to generate
                  \emph{efficient} and \emph{readable} code in a high level
                  object oriented language (Java, C++, ...).  SLAM is able to
                  generate prototypes that can be used to validate the
                  requirements with the user.  The additional advantage is
                  that the prototype is not throw-away because most part of
                  the generated code can be directly used and the other part
                  can be optimised with the additional help of assertions
                  automatically included.  },
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/finalcopy-rsp2003.ps.gz}
}
@inproceedings{hemo:2003:slam-xp,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Formal Extreme (and Extremely Formal) Programming},
  booktitle = {4th International Conference on Extreme Programming and
                  Agile Processes in Software Engineering, XP 2003},
  pages = {88-96},
  year = {2003},
  editor = {Michele Marchesi and Giancarlo Succi},
  series = {LNCS},
  number = {2675},
  month = may,
  address = {Genova, Italy},
  abstract = { This paper is an exploratory work were the authors study
                  how the technology of Formal Methods (FM) can interact with
                  agile process in general and with Extreme Programming (XP)
                  in particular.  Our thesis is that most of XP practices
                  (\emph{pair programming}, \emph{daily build}, \emph{the
                  simplest design} or \emph{the metaphor}) are technology
                  independent and therefore can be used in FM based
                  developments. Additionally, other essential pieces like
                  \emph{test first}, \emph{incremental development} and
                  \emph{refactoring} can be improved by using FM.  In the
                  paper we explore in a certain detail those pieces: when you
                  write a formal specification you are saying \emph{what} your
                  code must do, when you write a test you are doing the same
                  so the idea is to use formal specifications as tests.
                  Incremental development is quite similar to the refinement
                  process in FM: specifications evolve to code maintaining
                  previous functionality.  Finally FM can help to remove
                  redundancy, eliminate unused functionality and transform
                  obsolete designs into new ones, and this is refactoring.  },
  pdf = {http://babel.ls.fi.upm.es/~angel/papers/finalcopy-xp03.pdf}
}
@inproceedings{hemoma:2002:drapl:b,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro} and Noelia Maya},
  title = {Declarative Reflection and its Application as a Pattern
                  Language},
  booktitle = {Electronic Notes in Theoretical Computer Science},
  volume = {76},
  publisher = {Elsevier Science Publishers},
  editor = {Marco Comini and Moreno Falaschi},
  year = {2002},
  month = nov,
  abstract = { The paper presents the reflection facilities of the
                  specification language Slam-sl. Slam-sl is an object
                  oriented specification language where class methods are
                  specified by pre and postconditions. The reflection
                  capabilities allow managing these pre and postconditions in
                  specifications what means that semantic reflection is
                  possible. The range of interesting applications is very
                  wide: formal specification of interfaces and abstract
                  classes, specification of component based software,
                  formalization of design pattern, using Slam-sl as a pattern
                  language, etc.  The paper discusses the last two advantages
                  in some detail.},
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/finalcopy-entcs76-slam.ps.gz},
  url = {http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B75H1-4DDWJY1-DB-2&_cdi=13109&_user=885385&_orig=browse&_coverDate=11%2F30%2F2002&_sk=999239999&view=c&wchp=dGLbVtz-zSkWA&md5=93ab10fb3fcc627784dba6d9b75b1602&ie=/sdarticle.pdf}
}
@inproceedings{hemoma:2002:drapl,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro} and Noelia Maya},
  title = {Declarative Reflection and its Application as a Pattern
                  Language},
  booktitle = {11th. International Workshop on Functional and Logic
                  Programming (WFLP'02)},
  organization = {University of Udine},
  address = {Grado, Italy},
  editor = {Marco Comini and Moreno Falaschi},
  year = {2002},
  month = jun,
  abstract = { The paper presents the reflection facilities of the
                  specification language Slam-sl. Slam-sl is an object
                  oriented specification language where class methods are
                  specified by pre and postconditions. The reflection
                  capabilities allow managing these pre and postconditions in
                  specifications what means that semantic reflection is
                  possible. The range of interesting applications is very
                  wide: formal specification of interfaces and abstract
                  classes, specification of component based software,
                  formalization of design pattern, using Slam-sl as a pattern
                  language, etc.  The paper discusses the last two advantages
                  in some detail.},
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/finalcopy-wflp2002.ps.gz}
}
@inproceedings{hemo:2002:sloossdp,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Specifying in the Large: Object-oriented Specifications in
                  the Software Development Process},
  booktitle = {The Sixth Biennial World Conference on Integrated Design and
                  Process Technology (IDPT'02)},
  year = {2002},
  editor = {H. Ehrig, B. J. Krämer and A. Ertas},
  volume = {1},
  address = {Pasadena, California},
  month = jun,
  organization = {Society for Design and Process Science},
  note = {ISSN 1090-9389},
  abstract = { The paper discusses how formal methods, and, in particular,
                  object oriented specification languages can be integrated in
                  the software development process in an effective way. We
                  depart from an object specification language in the SLAM
                  system that combines characteristics of algebraic languages
                  as well as pre and postconditions for class methods
                  specification. We study how to specify classes as well as
                  the formal relations that class relationships must hold (in
                  particular, inheritance).  One of the main features of the
                  specification language is that it is supported by an
                  integrated environment that, among other facilities,
                  includes the generation of readable and (enough) efficient
                  imperative code. We also address how this translation can be
                  done and the extra capabilities of the environment regarding
                  the use of formal method in the development process, for
                  instance program validation.  },
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/finalcopy-idpt2002.ps.gz}
}
@inproceedings{hemo:2002:doofm,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {On the Design of an Object-oriented Formal Notation},
  booktitle = {Fourth Workshop on Rigorous Object Oriented Methods, ROOM 4},
  year = {2002},
  month = mar,
  organization = {King's College, London},
  abstract = { We consider that the application of formal methods in the
                  software development process is essential to obtain high
                  integrity products.  Despite the fact that arguments for
                  using formal methods, in practice it is clear that its use
                  is not widespread.  Slam is a software construction system
                  based on formal specifications. In this paper some features
                  of the formal specification language embedded in the Slam
                  system are presented: algebraic types, \emph{safe}
                  inheritance, generic polymorphism and collection
                  \emph{traversals}.  These features have in common that that
                  they rely on static information, they are well known
                  techniques, they are practical and relatively popular and
                  not all of them are usual in formal notations.},
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/finalcopy-room4.ps.gz}
}
@unpublished{mohe:2001:dpco,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Design Patterns as Class Operators},
  note = {Workshop on High Integrity Software Development at V Spanish
                  Conference on Software Engineering, JISBD'01},
  year = {2001},
  month = nov,
  address = {Almagro, Spain},
  abstract = {The paper presents a formalization of (some) design patterns
                  as operators between classes. A concrete design pattern is
                  understood as an operator that modifies certain classes into
                  the design proposed by the pattern. In such this way, we
                  present a way to understand design patterns in a formal
                  context, what aims for formal reasoning about
                  them. Furthermore, the view of design patterns as class
                  operators proposes a method to incorporate design patterns
                  into object oriented development tools.  It also can give
                  some hints to easily compose patterns , and to identify
                  design patterns in a given specification.},
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/design-patterns-as-class-operators-DSP-JISBD2001.ps.gz}
}
@inproceedings{mohe:2001:drapl:b,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Declarative Reflection and its Application as a Pattern
                  Language},
  booktitle = {I Jornadas sobre Programación y Lenguajes, PROLE 2001},
  pages = {179-197},
  year = {2001},
  month = nov,
  address = {Almagro, Spain},
  editor = {Fernando Orejas and Fernando Cuartero and Diego Cazorla},
  abstract = {The paper presents the reflection facilities of the
                  specification language Slam-sl. Slam-sl is an object
                  oriented specification language where class methods are
                  specified by pre and postconditions. The reflection
                  capabilities permit managing these pre and postconditions in
                  specifications what means that semantic reflection is
                  possible. The range of interesting applications is very
                  wide: formal specification of interfaces and abstract
                  classes, specification of component based software,
                  formalization of design pattern, using Slam-sl as a pattern
                  language, etc.  The paper discusses the last two advantages
                  in some detail.},
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/declarative_reflection-PROLE2001.ps.gz}
}
@unpublished{mohe:2001:drapl,
  author = {Juan José {Moreno-Navarro} and {Ángel} Herranz},
  title = {Declarative Reflection and its Application as a Pattern
                  Language},
  note = {Invited Session on ``Formalization of Object-Oriented
                  Methods, Patterns, and Frameworks'', The Fifth
                  Multi-Conference on Systemics, Cybernetics and Informatics
                  (SCI'2001)},
  address = {Orlando, Florida USA},
  month = jul,
  year = {2001},
  abstract = {The paper presents the reflection facilities of the
                  specification language Slam-sl. Slam-sl is an object
                  oriented specification language where class methods are
                  specified by pre and postconditions. The reflection
                  capabilities permit managing these pre and postconditions in
                  specifications what means that semantic reflection is
                  possible. The range of interesting applications is very
                  wide: formal specification of interfaces and abstract
                  classes, specification of component based software,
                  formalization of design pattern, using Slam-sl as a pattern
                  language, etc.  The paper discusses the last two advantages
                  in some detail.},
  postscript = {/papers/declarative_reflection-SCI2001.ps.gz}
}
@inproceedings{hemo:2000:tairppss,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Towards Automating the Iterative Rapid Prototyping Process
                  with the {SLAM} System},
  booktitle = {V Spanish Conference on Software Engineering},
  pages = {217-228},
  year = {2000},
  month = nov,
  abstract = {This paper shows the outlines of the Slam project, designed
                  for automating the Iterative Rapid Prototyping Process. The
                  Slam project system includes a very expressive object
                  oriented specification language that integrates
                  \emph{algebraic specifications} and \emph{model-based
                  specifications}. Class operations are defined by using rules
                  each of them with logical pre- and post-conditions but with
                  a functional flavour. The main novel feature of the system
                  is that contains a development environment that, among other
                  features, is able to generate (reasonable) efficient and
                  readable code in another high level object oriented language
                  (C++, Java, etc.). The generated code includes (part of) the
                  pre- and post-conditions as assertions, that can be
                  automatically checked in the debug mode execution of
                  programs. Slam can be used to generate prototypes that can
                  be used to validate the requirements with the user. The
                  additional advantage is that the prototype is not throw-away
                  because most part of the generated code can be used at it is
                  and the other part can be optimized with the additional help
                  of the declarative debugging of the modified code.},
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/slam-jis.ps.gz}
}
@inproceedings{hemo:2000:rflldip,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {On the Role of Functional-logic Languages for the Debugging
                  of Imperative Programs},
  booktitle = {9th International Workshop on Functional and Logic
                  Programming (WFLP 2000)},
  year = {2000},
  month = sep,
  organization = {Universidad Politécnica de Valencia},
  address = {Benicassim, Spain},
  abstract = {The paper presents some aspects of the debugging subsystem
                  of the ongoing project Slam where the language Curry plays a
                  significant role.  The Slam project is an attempt to
                  amalgamate most of the best facilities of declarative
                  languages to the development of imperative programs. The
                  Slam system is composed by i) an object oriented
                  specification language.  (Functional style) Rules are used
                  to define class operations each of them with logical pre and
                  post-conditions. ii) A development environment that, among
                  other features, is able to generate readable code in a high
                  level object oriented (imperative) language.  iii) The
                  generated code includes (part of) the pre and
                  post-conditions as assertions, that can be automatically
                  checked in the debug mode execution of programs. We
                  concentrate on the latter aspect. Many useful properties can
                  be expressed in the Slam language and these properties are
                  translated into a Curry program that is linked (via an
                  adequate interface) with the generated program. The Curry
                  execution is responsible for checking properties,
                  interacting with the debugging execution of the program.},
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/slam-curry.ps.gz}
}
@manual{hemo:st,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Slam-sl Tutorial},
  organization = {Grupo Babel, Facultad de Informática, Universidad
                  Politécnica de Madrid},
  address = {Campus de Montegancedo s/n, 28660, Boadilla del Monte,
                  Madrid, Spain},
  year = {2001},
  note = {\emph{Draft} based on Ángel Herranz's PhD. Thesis},
  abstract = {This paper shows the debugging facilities provided by the
                  Slam system.  The Slam system includes i) a specification
                  language that integrates \emph{algebraic specifications} and
                  \emph{model-based specifications} using the object oriented
                  model.  Class operations are defined by using rules each of
                  them with logical pre and postconditions but with a
                  functional flavour. ii) A development environment that,
                  among other features, is able to generate readable code in a
                  high level object oriented language.  iii) The generated
                  code includes (part of) the pre and postconditions as
                  assertions, that can be automatically checked in the debug
                  mode execution of programs. We focus on this last
                  aspect. The Slam language is expressive enough to describe
                  many useful properties and these properties are translated
                  into a Prolog program that is linked (via an adequate
                  interface) with the user program. The debugging execution of
                  the program interacts with the Prolog engine which is
                  responsible for checking properties.},
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/slam-sl-tutorial.ps.gz}
}
@inproceedings{hemo:2000:gdlppc,
  author = {{Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Generation of and Debugging with Logical Pre and Post
                  Conditions},
  booktitle = {Automated and Algorithmic Debugging 2000},
  year = {2000},
  month = aug,
  editor = {M. Ducasse},
  organization = {TU Munich},
  abstract = {This paper shows the debugging facilities provided by the
                  SLAM system.  The SLAM system includes i) a specification
                  language that integrates \emph{algebraic specifications} and
                  \emph{model-based specifications} using the object oriented
                  model.  Class operations are defined by using rules each of
                  them with logical pre and postconditions but with a
                  functional flavour. ii) A development environment that,
                  among other features, is able to generate readable code in a
                  high level object oriented language.  iii) The generated
                  code includes (part of) the pre and postconditions as
                  assertions, that can be automatically checked in the debug
                  mode execution of programs.  We focus on this last
                  aspect. The SLAM language is expressive enough to describe
                  many useful properties and these properties are translated
                  into a Prolog program that is linked (via an adequate
                  interface) with the user program. The debugging execution of
                  the program interacts with the Prolog engine which is
                  responsible for checking properties.  },
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/slam-debug.ps.gz}
}
@inproceedings{carro:marinno:herranz:moreno:2004:tfm,
  author = {Manuel Carro and Julio Mariño and \'{A}ngel Herranz and Juan
                  José {Moreno-Navarro}},
  title = {Teaching How to Derive Correct Concurrent Programs (from
                  State-based Specifications and Code Patterns)},
  booktitle = {Teaching Formal Methods, CoLogNET/FME Symposium, TFM 2004,
                  Ghent, Belgium},
  pages = {85--106},
  year = 2004,
  editor = {C.N. Dean and R.T. Boute},
  volume = 3294,
  series = {LNCS},
  publisher = {Springer},
  note = {ISBN 3-540-23611-2}
}
@article{herranz:marinno:2004:novatica,
  author = {\'{A}ngel Herranz and Julio Mariño},
  title = {Por otra ruta, por favor},
  journal = {Novática},
  year = 2004,
  month = aug,
  volume = {1},
  number = 170,
  pages = {73--75},
  note = {Contribución a la columna "Programar es Crear"}
}
@article{carro:herranz:marinno:sanchez:2003:novatica,
  author = {\'{A}ngel Herranz and Manuel Carro and Julio Mariño and
                  Pablo {Sánchez Torralba}},
  title = {Almejas gigantes e interfaces de usuario},
  journal = {Novática},
  year = 2003,
  volume = {1},
  number = 161,
  month = feb,
  pages = {70--73},
  note = {Contribución a la columna "Programar es Crear"}
}
@article{carro:herranz:marinno:sanchez:2002:novatica,
  author = {\'{A}ngel Herranz and Manuel Carro and Julio Mariño and
                  Pablo {Sánchez Torralba}},
  title = {No taléis el bosque por culpa de los árboles},
  journal = {Novática},
  year = 2002,
  month = oct,
  volume = {1},
  number = 159,
  pages = {74--77},
  note = {Contribución a la columna "Programar es Crear"}
}
@inproceedings{AGPDLF96:Moreno:TypeClassesCurry,
  title = {Adding Type-Classes to Functional-logic Languages},
  booktitle = {APPIA-GULP-PRODE'96},
  organization = {Universidad del País Vasco},
  year = {1996},
  editor = {M. Martelli and M. Navarro},
  publisher = {Summer Courses, Basque Country University},
  pages = {427-438},
  author = {J.J. {Moreno-Navarro} and J. Mariño and J. García Martín and
                  {Ángel} Herranz and A. del Pozo}
}
@inproceedings{MHM93,
  author = {Julio Mariño and {Ángel} Herranz and Juan José {Moreno-Navarro}},
  title = {Demandedness Analysis with Dependence Information for Lazy
                  Narrowing},
  editor = {W. Winsborough and S. Michaylov},
  booktitle = {Workshop on Global Compilation, International Logic
                  Programming Symposium October 26-30, 1993, Vancouver, BC,
                  Canada},
  year = {1993},
  organization = {Association for Logic Programming and Simon Fraser
                  University},
  pages = {99--114},
  month = oct,
  note = {Penn State University Technical Report}
}
@inproceedings{HM93,
  author = {Julio Mariño and {Ángel} Herranz},
  title = {Specialized Compilation of Lazy Functional Logic Programs},
  year = {1993},
  pages = {39--55},
  organization = {Instituto de Investigación en Inteligencia Artificial, CSIC},
  booktitle = {Segundo Congreso Nacional de Programación Declarativa -- 2nd
                  Spanish Conference on Declarative Programming (ProDe'93)}
}
@unpublished{camahemo:2004:fulltcp,
  author = {Manuel Carro and Julio Mariño and {Ángel} Herranz and Juan
                  José {Moreno-Navarro}},
  title = {Teaching How to Derive Correct Concurrent Programs from
                  State-Based Specifications},
  note = {Full paper},
  year = {2004},
  abstract = { The fun of teaching and learning concurrent programming is
                  sometimes darkened by the difficulty in getting concurrent
                  programs to work right.  In line with other programming
                  subjects in our department, we advocate the use of formal
                  specifications to state clearly how a concurrent program
                  must behave, to reason about this behavior, and to be able
                  to produce code from specifications in a semi-automatic
                  fashion.  We argue that a mild form of specification not
                  only makes it possible to get programs running easier, but
                  it also introduces students to a quite systematic way of
                  approaching programming: reading and understanding
                  specifications is seen as an unavoidable step in the
                  programming process, as they are really the only place where
                  the expected conduct of the system is completely described.
                  By using formal techniques in these cases, where it is
                  undoubtedly appropriate, we introduce formality without the
                  need to resort to justifications with artificial or overly
                  complicated examples.  },
  optkey = {},
  month = sep,
  optannote = {},
  postscript = {http://babel.ls.fi.upm.es/~angel/papers/tfm2004-full.ps.gz}
}

This file was generated by bibtex2html 1.94.