@inproceedings{susana:2007:robocup_IEEE,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  author = {Mu{\~{n}}oz-Hern{\'{a}}ndez, Susana and Wiratna Sari Wiguna},
  title = {Fuzzy Prolog as Cognitive Layer in RoboCupSoccer},
  revisores = {yes},
  descripcion = {},
  booktitle = {IEEE Symposium on Computational Intelligence and Games (2007
                  IEEE Symposia Series in Computational Intelligence)},
  pages = {340-345},
  year = {2007},
  series = {IEEE},
  address = {Honolulu, Hawaii},
  month = {April}
}
@inproceedings{susana:2007:robocup_IFSA,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  author = {Mu{\~{n}}oz-Hern{\'{a}}ndez, Susana and Wiratna Sari Wiguna},
  title = {Fuzzy Cognitive Layer in RoboCupSoccer},
  revisores = {yes},
  booktitle = {12th International Fuzzy Systems Association World Congress
                  (IFSA 2007). Foundations of Fuzzy Logic and Soft Computing},
  pages = {635-645},
  year = {2007},
  optnumber = {4529},
  optseries = {LNAI},
  address = {Canc{\'u}n, M{\'e}xico},
  month = {June},
  publisher = {Springer}
}
@inproceedings{DBLP:conf/tlca/LiptonN07,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  revisores = {yes},
  author = {James Lipton and Susana Nieva},
  title = {Higher-Order Logic Programming Languages with
                  Constraints: A Semantics},
  booktitle = {Typed Lambda Calculi and Applications},
  descripcion = {Definimos una sem{\'{a}}ntica tipo Kripke para un lenguaje
                  de programaci{\'{o}}n l{\'{o}}gica de orden superior con
                  restricciones, basado en la Teor{\'{i}}a de Tipos de
                  Church y un formalismo gen{\'{e}}rico de restricciones.},
  pages = {272--289},
  address = {Paris, France},
  month = {June 26--28},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 4583,
  year = 2007,
  isbn = {978-3-540-73227-3}
}
@article{pareja:marinno:2007:novatica:papiroflexia,
  tipoactividad = {Art{\'{i}}culos en revistas},
  internacional = {no},
  author = {Crist{\'{o}}bal Pareja Flores and Julio Mari{\~{n}}o Carballo},
  title = {Papiroflexia},
  journal = {Nov{\'{a}}tica},
  issn = {0211-2124},
  year = 2007,
  volume = 1,
  number = 189,
  pages = {73--75},
  month = sep,
  descripcion = {Contribuci{\'{o}}n semiperi{\'{o}}dica a la columna "Programar es Crear"
                  de la revista Nov{\'{a}}tica. En esta ocasi{\'{o}}n describimos la
                  soluci{\'{o}}n al problema E del Concurso de Programaci{\'{o}}n de la
                  Comunidad de Madrid del a{\~{n}}o 2006.}
}
@techreport{xmc:2007:_study_of_exist_codin_rule,
  tipoactividad = {Otras publicaciones},
  internacional = {yes},
  author = {Julio Mari{\~{n}}o and {{\'{A}}ngel} Herranz and Lars-{\AA}ke Fredlund and
                  Manuel Carro and Pablos-Ceruelo, V{\'{i}}ctor and Guillem Marpons and Juan
                  Jos{\'{e}} {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{\'{o}}n, relaci{\'{o}}n de riesgos de software m{\'{a}}s comunes y
                  resultados de encuesta a socios del proyecto {GlobalGCC}.},
  institution = {Facultad de Inform{\'{a}}tica, Universidad Polit{\'{e}}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 {{\'{A}}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 {{\'{A}}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{\~{n}}o and {{\'{A}}ngel} Herranz and
                  Lars-{\AA}ke Fredlund and Manuel Carro and Juan Jos{\'{e}}
                  {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}
}
@unpublished{garcia:2007:acsd,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  author = {{{\'{A}}lvaro} {Garc{\'{i}}a-P{\'{e}}rez} and Nelson {Medinilla Mart{\'{i}}nez}},
  title = {The Ambiguity Criterion in Software Design},
  url = {http://se.cs.toronto.edu/IWLU/program.html},
  note = {International Workshop on Living with Uncertainties 2007
                  (IWLU'07), Co-located with the 22nd International conference
                  on Automated Software engineering (ASE'07)},
  month = nov,
  year = {2007}
}
@article{gabbay:frelog,
  tipoactividad = {Art{\'{i}}culos en revistas},
  internacional = {yes},
  author = {Murdoch J. Gabbay},
  title = {Fresh Logic: proof-theory and semantics for FM and nominal
                  techniques},
  journal = {Journal of Applied Logic},
  year = {2007},
  url = {http://www.gabbay.org.uk/papers/frelog.pdf},
  optdescripcion = {},
  optissn = {},
  optkey = {},
  volume = {5},
  number = {2},
  pages = {356-387},
  optmonth = {},
  optnote = {},
  optannote = {},
  abstract = {In this paper we introduce Fresh Logic, a natural deduction
                  style first-order logic extended with term-formers and
                  quantifiers derived from the FM-sets model of names and
                  binding in abstract syntax. Fresh Logic can be classical or
                  intuitionistic depending on whether we include a law of
                  excluded middle; we present a proof-normalisation procedure
                  for the intuitionistic case and a semantics based on Kripke
                  models in FM-sets for which it is sound and complete.}
}
@article{gabbay:genmn,
  tipoactividad = {Art{\'{i}}culos en revistas},
  internacional = {yes},
  author = {Murdoch J. Gabbay},
  title = {A general mathematics of names},
  journal = {Information and Computation},
  year = {2007},
  optdescripcion = {},
  optissn = {},
  optkey = {},
  volume = {205},
  number = {7},
  pages = {982-1011},
  optmonth = {},
  optnote = {},
  optannote = {},
  url = {http://www.gabbay.org.uk/papers/genmn.pdf},
  abstract = {We introduce FMG (Fraenkel-Mostowski Generalised) set
                  theory, a generalisation of FM set theory which allows
                  binding of infinitely many names instead of just finitely
                  many names. We apply this generalisation to show how three
                  presentations of syntax--de Bruijn indices, FM sets, and
                  name-carrying syntax--have a relation generalising to all
                  sets and not only sets of syntax trees. We also give
                  syntax-free accounts of Barendregt representatives, scope
                  extrusion, and other phenomena associated to
                  $\alpha$-equivalence.  Our presentation uses a novel
                  presentation based not on a theory but on a concrete model
                  U.}
}
@article{gabbay:nomr-jv,
  tipoactividad = {Art{\'{i}}culos en revistas},
  internacional = {yes},
  author = {Maribel Fern\'{a}ndez and Murdoch J. Gabbay},
  title = {Nominal Rewriting (journal version)},
  journal = {Information and Computation},
  year = {2007},
  optdescripcion = {},
  optissn = {},
  optkey = {},
  volume = {205},
  number = {6},
  pages = {917-965},
  optmonth = {},
  optnote = {},
  optannote = {},
  url = {http://www.gabbay.org.uk/papers/nomr-jv.pdf},
  abstract = {Nominal rewriting is based on the observation that if we add
                  support for $\alpha$-equivalence to first-order syntax using
                  the nominal-set approach, then systems with binding,
                  including higher-order reduction schemes such as
                  $\lambda$-calculus beta-reduction, can be smoothly
                  represented. Nominal rewriting maintains a strict
                  distinction between variables of the object-language (atoms)
                  and of the meta-language (variables or unknowns). Atoms may
                  be bound by a special abstraction operation, but variables
                  cannot be bound, giving the framework a pronounced
                  first-order character, since substitution of terms for
                  variables is not capture-avoiding. We show how good
                  properties of first-order rewriting survive the extension,
                  by giving an efficient rewriting algorithm, a critical pair
                  lemma, and a confluence theorem for orthogonal systems.}
}
@article{gabbay:hientt,
  tipoactividad = {Art{\'{i}}culos en revistas},
  internacional = {yes},
  author = {Murdoch J. Gabbay},
  title = {Hierarchical Nominal Terms and their Theory of
                  Rewriting},
  journal = {Electronic Notes in Theoretical Computer Science},
  year = 2007,
  issn = {1571-0661},
  volume = 174,
  number = 5,
  pages = {37-52},
  url = {http://www.gabbay.org.uk/papers/hientt.pdf},
  abstract = {Nominal rewriting introduced a novel method of
                  specifying rewriting on syntax-with-binding. We
                  extend this treatment of rewriting with hierarchy of
                  variables representing increasingly 'meta-level'
                  variables, e.g. in hierarchical nominal term
                  rewriting the meta-level unknowns (representing
                  unknown terms) in a rewrite rule can be 'folded
                  into' the syntax itself (and rewritten). To the
                  extent that rewriting is a mathematical
                  meta-framework for logic and computation, and
                  nominal rewriting is a framework with native support
                  for binders, hierarchical nominal term rewriting is
                  a meta-to-the-omega level framework for logic and
                  computation with binders.}
}
@inproceedings{gabbay:forcie,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  author = {Murdoch J. Gabbay and Aad Mathijssen},
  title = {A Formal Calculus for Informal Equality with Binding},
  optrevisores = {},
  optdescripcion = {},
  optisbn = {},
  optcrossref = {},
  optkey = {},
  booktitle = {Proceedings of WOLLIC'07},
  pages = {162-176},
  year = {2007},
  opteditor = {},
  volume = {4576},
  optnumber = {},
  series = {Lecture Notes in Computer Science},
  address = {},
  optmonth = {},
  optorganization = {},
  optpublisher = {},
  optnote = {},
  optannote = {},
  url = {http://www.gabbay.org.uk/papers/forcie.pdf},
  abstract = {In informal mathematical usage we often reason using
                  languages with binding. We usually find ourselves placing
                  capture-avoidance constraints on where variables can and
                  cannot occur free. We describe a logical derivation system
                  which allows a direct formalisation of such assertions,
                  along with a direct formalisation of their constraints. We
                  base our logic on equality, probably the simplest available
                  judgement form. In spite of this, we can axiomatise systems
                  of logic and computation such as first-order logic or the
                  lambda-calculus in a very direct and natural way. We
                  investigate the theory of derivations, prove a suitable
                  semantics sound and complete, and discuss existing and
                  future research.}
}
@inbook{hemo:2007:mrdps,
  author = {{{\'{A}}ngel} Herranz and Juan Jos{\'{e}} {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{\'{i}}tulos de libro},
  internacional = {yes},
  description = {El principal objetivo del cap{\'{i}}tulo es el estudio de
                  la descripci{\'{o}}n de patrones de dise{\~{n}}o como operadores
                  matem{\'{a}}ticos sobre clases. Adem{\'{a}}s, se describen dos
                  posibles aplicaciones de la formalizaci{\'{o}}n:
                  razonamiento sobre patrones de dise{\~{n}}o y la
                  refactorizaci{\'{o}}n autom{\'{a}}tica de los dise{\~{n}}os utilizando
                  los operadores de clases definidos.},
  pdf = {http://babel.ls.fi.upm.es/~angel/papers/taibichapter-finalcopy.pdf}
}
@article{mahemo:2007:dapp,
  tipoactividad = {Art{\'{i}}culos en revistas},
  internacional = {yes},
  author = {Julio Mari{\~{n}}o and {{\'{A}}ngel} Herranz and Juan Jos{\'{e}}
                  {Moreno-Navarro}},
  title = {Demand 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{\'{a}}lisis de demanda pretende determinar en tiempo de
                  compilaci{\'{o}}n qu{\'{e}} c{\'{a}}lculos van a ser realmente utilizados
                  durante la ejecuci{\'{o}}n de un programa. Esta informaci{\'{o}}n puede
                  ser muy relevante para la implementaci{\'{o}}n de lenguajes
                  l{\'{o}}gico-funcionales.  Este trabajo propone un marco sem{\'{a}}ntico
                  de predicados parciales, que podr{\'{i}}amos ver como
                  realizaciones constructivas de ideales sobre un cierto
                  dominio. Con esto conseguimos dar una presentaci{\'{o}}n concisa y
                  unificada de una familia de an{\'{a}}lisis de demanda,
                  relacionarlo con otras propuestas, ideas para su
                  implementaci{\'{o}}n y, finalmente, demostrar la correcci{\'{o}}n de una
                  propuesta anterior basada en la resoluci{\'{o}}n de ecuaciones de
                  demanda.}
}
@article{DBLP:journals/entcs/AriasMP07,
  author = {Emilio Jes{\'u}s {Gallego Arias} and Julio
                  {Mari{\~n}o-Carballo} and Jos{\'e} Mar\'{\i}a {Rey Poza}},
  title = {A Proposal for Disequality Constraints in Curry},
  journal = {Electr. Notes Theor. Comput. Sci.},
  volume = {177},
  year = {2007},
  pages = {269-285},
  issn = {1571-0661},
  ee = {http://dx.doi.org/10.1016/j.entcs.2007.01.014},
  abstract = {We describe the introduction of disequality constraints over
                  algebraic data terms in the functional logic language Curry,
                  and their implementation in Sloth, our Curry compiler. This
                  addition extends the standard definition of Curry in several
                  ways. On one hand, we provide a disequality counterpart to
                  the constraint equality operator (=:=). Secondly, boolean
                  equality operators are also redefined to cope with
                  constructive disequality information, which leads to a more
                  symmetric design w.r.t. the existing one. Semantically
                  speaking, our implementation is very similar to previous
                  proposals, although there are some novel aspects. One of
                  them is that the implementation is partly based on an
                  existing finite domain (FD) constraint solver, which
                  provides a more efficient execution in some examples and,
                  more important, the first complete implementation of
                  disequality constraints over finite types. A detailed
                  description of the finite type case is provided, including:
                  (i) the use of the FD solver; (ii) an algorithm for analysing
                  cardinality of types, and (iii) how to deal with cardinality
                  information at run time. Some benchmarks, an operational
                  semantics minimally extending the one in the Curry draft,
                  and a moderately detailed description of the implementation
                  complete the paper.},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{Genericsem,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  revisores = {yes},
  author = {Emilio Jes{\'u}s {Gallego Arias} and Julio
                  {Mari{\~n}o-Carballo} and Jos{\'e} Mar\'{\i}a {Rey Poza}},
  title = {A Generic Semantics for Constraint Functional Logic
                  Programming},
  booktitle = {Proc.\ of the 16th Int'l Workshop on Functional and
                  (Constraint) Logic Programming (WFLP 2007)},
  descripcion = {Proponemos una sem{\'{a}}ntica operacional para programas l{\'{o}}gico
                  funcionales perezosos con restricciones que es gen{\'{e}}rica en
                  tanto que permite la integraci{\'{o}}n de diferentes resolvedores
                  de restricciones en un n{\'{u}}cleo com{\'{u}}n de una manera bastante
                  limpia. El dise{\~{n}}o de esta sem{\'{a}}ntica trata de satisfacer dos
                  principios aparentemente contradictorios: la necesidad de
                  dar soporte a la evaluaci{\'{o}}n perezosa desde el resolvedor de
                  restricciones y el principio de caja negra aplicado al
                  dise{\~{n}}o de la relaci{\'{o}}n entre el resolvedor y el motor de
                  inferencia.},
  year = 2007,
  month = {June 25},
  address = {Paris, France}
}
@mastersthesis{Relunif,
  author = {Emilio Jes{\'u}s {Gallego Arias}},
  title = {Relational Unification},
  school = {Facultad de Inform{\'{a}}tica, Universidad Polit{\'{e}}cnica de Madrid},
  year = 2007,
  month = oct,
  note = {Advisor: James Lipton}
}
@inproceedings{pni:tfp07:adtfunctor:proceedings,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  revisores = {yes},
  author = {Pablo Nogueira},
  title = {When is an Abstract Data Type a Functor?},
  booktitle = {Proceedings of the 7th {S}ymposium on {T}rends in {F}unctional
                  {P}rogramming - {TFP}'06},
  pages = {217-231},
  optpublisher = {left out on purpose},
  year = 2007,
  month = {April 19-21},
  address = {Nottingham, UK},
  editor = {Henrik Nilsson},
  note = {Winner of Best Student Paper Award},
  abstract = {A parametric algebraic data type is a functor when we can
                  apply a function to its data components while satisfying
                  certain equations. We investigate whether parametric
                  abstract data types can be functors. We provide a general
                  definition for their map operation that needs only satisfy
                  one equation. The definability of this map depends on
                  properties of interfaces and is a sufficient condition for
                  functoriality. Instances of the definition for particular
                  abstract types can then be constructed using their axiomatic
                  semantics. The definition and the equation can be adapted to
                  determine, necessarily and sufficiently, whether an ADT is a
                  functor for a given implementation},
  pdf = {http://babel.ls.fi.upm.es/~pablo/Papers/adt-functors.pdf}
}
@incollection{pni:tfp07:adtfunctor:chapter,
  tipoactividad = {Cap{\'{i}}tulos de libros},
  internacional = {yes},
  author = {Pablo Nogueira},
  title = {When is an Abstract Data Type a Functor?},
  booktitle = {Trends in Functional Programming},
  isbn = {978-1-84150-188-8},
  pages = {217-231},
  publisher = {Intellect},
  year = 2007,
  month = {September 30},
  editor = {Henrik Nilsson},
  volume = 7,
  chapter = 13,
  note = {Winner of Best Student Paper Award},
  abstract = {A parametric algebraic data type is a functor when we can
                  apply a function to its data components while satisfying
                  certain equations. We investigate whether parametric
                  abstract data types can be functors. We provide a general
                  definition for their map operation that needs only satisfy
                  one equation. The definability of this map depends on
                  properties of interfaces and is a sufficient condition for
                  functoriality. Instances of the definition for particular
                  abstract types can then be constructed using their axiomatic
                  semantics. The definition and the equation can be adapted to
                  determine, necessarily and sufficiently, whether an ADT is a
                  functor for a given implementation},
  pdf = {http://babel.ls.fi.upm.es/~pablo/Papers/adt-functors.pdf}
}
@article{fredlund_svensson:mcErlangSIGPLAN,
  tipoactividad = {Art{\'{i}}culos en revistas},
  internacional = {yes},
  author = {Lars-{\AA}ke Fredlund and H. Svensson},
  title = {Mc{E}rlang: a model checker for a distributed
                  functional programming language},
  revisores = {yes},
  journal = {ACM SIGPLAN Notices},
  issn = {0362-1340},
  year = 2007,
  abstract = {We present a model checker for verifying distributed
                  programs written in the Erlang programming
                  language. Providing a model checker for Erlang is
                  especially rewarding since the language is by now
                  being seen as a very capable platform for developing
                  industrial strength distributed applications with
                  excellent failure tolerance characteristics. In
                  contrast to most other Erlang verification attempts,
                  we provide support for a very substantial part of
                  the language. The model checker has full Erlang data
                  type support, support for general process
                  communication, node semantics (inter-process behave
                  subtly different from intra-process communication),
                  fault detection and fault tolerance through process
                  linking, and can verify programs written using the
                  OTP Erlang component library (used by most modern
                  Erlang programs).  As the model checking tool is
                  itself implemented in Erlang we benefit from the
                  advantages that a (dynamically typed) functional
                  programming language offers: easy prototyping and
                  experimentation with new verification algorithms,
                  rich executable models that use complex data
                  structures directly programmed in Erlang, the
                  ability to treat executable models interchangeably
                  as programs (to be executed directly by the Erlang
                  interpreter) and data, and not least the possibility
                  to cleanly structure and to cleanly combine various
                  verification sub-tasks.  In the paper we discuss the
                  design of the tool and provide early indications on
                  its performance.},
  issn = {0362-1340},
  volume = 42,
  number = 9,
  pages = {125-136}
}
@inproceedings{fredlund_svensson:mcErlangICFP,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  revisores = {yes},
  author = {Lars-{\AA}ke Fredlund and H. Svensson},
  title = {Mc{E}rlang: a model checker for a distributed
                  functional programming language},
  booktitle = {Proceedings of the 12th ACM SIGPLAN International
                  conference on functional programming (ICFP 2007)},
  abstract = {We present a model checker for verifying distributed
                  programs written in the Erlang programming
                  language. Providing a model checker for Erlang is
                  especially rewarding since the language is by now
                  being seen as a very capable platform for developing
                  industrial strength distributed applications with
                  excellent failure tolerance characteristics. In
                  contrast to most other Erlang verification attempts,
                  we provide support for a very substantial part of
                  the language. The model checker has full Erlang data
                  type support, support for general process
                  communication, node semantics (inter-process behave
                  subtly different from intra-process communication),
                  fault detection and fault tolerance through process
                  linking, and can verify programs written using the
                  OTP Erlang component library (used by most modern
                  Erlang programs).  As the model checking tool is
                  itself implemented in Erlang we benefit from the
                  advantages that a (dynamically typed) functional
                  programming language offers: easy prototyping and
                  experimentation with new verification algorithms,
                  rich executable models that use complex data
                  structures directly programmed in Erlang, the
                  ability to treat executable models interchangeably
                  as programs (to be executed directly by the Erlang
                  interpreter) and data, and not least the possibility
                  to cleanly structure and to cleanly combine various
                  verification sub-tasks.  In the paper we discuss the
                  design of the tool and provide early indications on
                  its performance.},
  isbn = {978-1-59593-815-2},
  year = 2007,
  month = oct
}
@inproceedings{svensson_fredlund:accsem,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  revisores = {yes},
  author = {H. Svensson and Lars-{\AA}ke Fredlund},
  title = {A more accurate semantics for distributed {E}rlang},
  booktitle = {Proceedings of the 2007 ACM SIGPLAN Erlang Workshop},
  abstract = {In order to formally reason about distributed Erlang
                  systems, it is necessary to have a formal semantics.
                  In a previous paper we have proposed such a
                  semantics for distributed Erlang. However, recent
                  work with a model checker for Erlang revealed that
                  the previous attempt was not good enough. In this
                  paper we present a more accurate semantics includes
                  several modifications and additions to the semantics
                  for distributed Erlang proposed by Claesson and
                  Svensson in 2005, which in turn is an extension to
                  Fredlund's formal single-node semantics for
                  Erlang. The most distinct addition to the previous
                  semantics is the possibility to correctly model
                  disconnected nodes.},
  year = 2007,
  isbn = {978-1-59593-675-2},
  month = oct
}
@inproceedings{svensson_fredlund:pitfalls,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  revisores = {yes},
  author = {H. Svensson and Lars-{\AA}ke Fredlund},
  year = 2007,
  isbn = {978-1-59593-675-2},
  month = oct,
  abstract = {We investigate the distributed part of the Erlang
                  programming language, with an aim to develop robust
                  distributed systems and algorithms running on top of
                  Erlang runtime systems. Although the step to convert
                  an application running on a single node to a fully
                  distributed (multi-node) application is deceptively
                  simple (changing calls to \texttt{spawn} so that
                  processes are spawned on different nodes), there are
                  some corner cases in the Erlang language and API
                  where the introduction of distribution can cause
                  problems. In this paper we discuss a number of such
                  pitfalls, where the semantics of communicating
                  processes differs significantly depending if the
                  processes reside on the same node or not, we also
                  provide some guidelines for safe programming of
                  distributed systems.},
  title = {Programming distributed {E}rlang applications:
                  pitfalls and recipes},
  booktitle = {Proceedings of the 2007 ACM SIGPLAN Erlang Workshop}
}
@inproceedings{fredlund_penas:mcErlangVodka,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  revisores = {yes},
  isbn = {978-3-540-75866-2},
  author = {Lars-{\AA}ke Fredlund and J. {S{\'{a}}nchez Penas}},
  title = {Model checking a video-on-demand server using
                  Mc{E}rlang},
  booktitle = {Proceedings of the 11th International Conference on
                  Computer Aided Systems Theory (Eurocast 2007)},
  abstract = {The article describes a method to obtain performance
                  measurements from complex distributed systems using
                  a model checking approach.  We illustrate the
                  approach by applying it to a video-on-demand
                  application developed in Erlang.  To obtain
                  performance measurements concerning e.g.\ streaming
                  capacity, and identify system bottlenecks, we used
                  the McErlang model checker which implements a large
                  part of the Erlang API. Answers to capacity queries
                  are computed as measures over paths in the system
                  state graph, and the combination of an on-the-fly
                  model checker (not requiring the generation of the
                  complete state graph) with a powerful language
                  (Erlang itself) for expressing correctness claims,
                  made it possible to analyse substantially sized
                  systems.},
  volume = 4739,
  series = {LNCS},
  publisher = {Springer},
  year = 2007,
  month = feb
}
@proceedings{fredlund_thompson:Erlang07,
  tipoactividad = {Libros},
  internacional = {yes},
  editor = {S. Thompson and Lars-{\AA}ke Fredlund},
  booktitle = {Proceedings of the 2007 ACM SIGPLAN Erlang Workshop},
  title = {Proceedings of the 2007 ACM SIGPLAN Erlang Workshop},
  year = 2007,
  month = oct,
  abstract = {Proceedings of the 2007 ACM SIGPLAN Erlang Workshop.},
  editorial = {ACM Press},
  isbn = {978-1-59593-675-2}
}

This file was generated by bibtex2html 1.98.