@proceedings{AGN:PROLE:2011,
  tipoactividad = {Libros},
  internacional = {no},
  title = {Actas de las {XI} {J}ornadas sobre {P}rogramaci{\'{o}}n y
                  {L}enguajes - {PROLE'11}},
  year = {2011},
  abstract = {Actas del congreso},
  pdf = {http://www.sistedes.es/ficheros/actas-conferencias/PROLE/2011.pdf},
  isbn = {978-84-9749-487-8},
  editor = {{Purificaci{\'{o}}n Arenas} and {Victor M. Gul{\'{i}}as} and {Pablo
                  Nogueira}},
  month = {September 5--7},
  publisher = {Universidade da Coru{\~{n}}a}
}
@book{WFLP2010,
  editor = {Julio Mari{\~{n}}o},
  title = {Functional and Constraint Logic Programming, 19th International Workshop, Revised Selected Papers},
  publisher = {Springer Verlag},
  year = 2011,
  volume = 6559,
  series = {LNCS}
}
@inproceedings{fbf2011prole,
  author = {{\'{A}}lvaro Fern{\'{a}}ndez-D{\'{i}}az and Clara Benac and Lars-\AA
                  ke Fredlund},
  title = {Erlang Implementation and Formal Verification of a
                  Distributed {MAS} Protocol},
  booktitle = {XI Jornadas sobre Programaci{\'{o}}n y Lenguajes, PROLE2011},
  year = 2011,
  editor = {Nogueira and Arenas and Gul{\'{i}}as},
  publisher = {Universidades da Coru{\~{n}}a}
}
@mastersthesis{apolo2011tfc,
  author = {{Miguel {\'{A}}ngel} {Polo Mancera}},
  title = {Polimorfismo Ad-hoc en un Lenguaje L{\'{o}}gico Funcional},
  school = {Facultad de Inform{\'{a}}tica, Universidad Polit{\'{e}}cnica de Madrid},
  year = 2011,
  month = {July},
  note = {Supervised by Julio Mari{\~{n}}o (in Spanish)}
}
@incollection{gabbay2011barringer,
  author = {Murdoch J. Gabbay},
  title = {Festschrift in Honour of {H}oward {B}arringer},
  chapter = {Stone Duality for First-order Logic: a Nominal
                  Approach to Logic and Topology},
  year = {2011},
  optmonth = {december}
}
@inproceedings{fdez-soriano11:_tool_integ_const_logic_progr_spread,
  tipoactividad = {Ponencias en congresos},
  internacional = {no},
  author = {Ana Mar{\'{i}}a {Fern{\'{a}}ndez-Soriano} and Julio Mari{\~{n}}o and {{\'{A}}ngel} Herranz},
  title = {A Tool for the Integration of Constraint Logic Programming in Spreadsheets},
  booktitle = {Actas XI Jornadas sobre Programaci{\'{o}}n y Lenguajes},
  pages = {243-252},
  year = 2011,
  editor = {{Purificaci{\'{o}}n} Arenas and {V{\'{i}}ctor M.} Gul{\'{i}}as and Pablo Nogueira},
  address = {A Coru{\~{n}}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 = {{{\'{A}}ngel} Herranz and Julio Mari{\~{n}}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}
}
@unpublished{fre-euc1,
  tipoactividad = {Cursos, seminarios y tutoriales},
  internacional = {yes},
  author = {Lars-{\AA}ke Fredlund},
  title = {{McErlang}},
  note = {Tutorial talk at the Erlang User Conference 2011},
  description = {Developing reliable concurrent software is a hard task given the
inherent non-deterministic nature of concurrent systems. A technique
which is often used to check that a concurrent program fulfils a set
of desirable properties is model checking. In model checking, all the
states of a concurrent system are systematically explored.

McErlang is a tool which helps finding bugs in concurrent Erlang
programs using model checking. In this tutorial we
will illustrate the use of McErlang through simple examples.
A new functionality is the integration of QuickCheck and McErlang;
we show how the same QuickCheck state maching model can be checked
either using QuickCheck, QuickCheck/Pulse or QuickCheck+McErlang,
and explain the trade-offs of using the tools.},
  url = {http://www.erlang-factory.com/conference/ErlangUserConference2011/programme/39},
  location = {Stockholm, Sweden},
  month = {November 4},
  year = {2011}
}
@unpublished{fre-euc2,
  tipoactividad = {Cursos, seminarios y tutoriales},
  internacional = {yes},
  author = {Lars-{\AA}ke Fredlund},
  title = {{Erlang QuickCheck and Java}},
  note = {Tutorial talk at the Erlang User Conference 2011},
  description = {In this tutorial we show how Java libraries can be debugged using Erlang
QuickCheck. To avoid having to write a lot of boilerplate code when calling
Java methods from Erlang, we use a new library implemented on top
of Jinterface. The approach will be illustrated by testing a Java library
using a QuickCheck state machine (eqc_statem) specification.},
  url = {http://www.erlang-factory.com/conference/ErlangUserConference2011/programme/39},
  location = {Stockholm, Sweden},
  month = {November 4},
  year = {2011}
}
@mastersthesis{2011:avalor,
  author = {Fern{\'{a}}ndez D{\'{i}}az, {\'{A}}lvaro},
  title = {Static Partial Order Reduction for Probabilistic Systems},
  school = {Fakult\"at f{\"u}r Informatik, Technische Universit\"at
                  Dresden},
  year = {2011},
  month = {July 29},
  url = {http://www.emcl-study.eu/graduates.html},
  internacional = {yes},
  note = {Advisor: Christel Baier, Calificaci{\'{o}}n:
                  Sobresaliente},
  pdf = {http://babel.ls.fi.upm.es/~avalor/papers/masterThesis.pdf},
  calificacion = {1.3 (German Grading System)},
  abstract = {The present Master's thesis seeks the development and analysis of
static partial order reduction techniques for the models of
probabilistic systems. The properties of those systems can be verified
via model checking techniques. Model checking suffers from the problem
known as State Space Explosion, which can make the verification
process intractable. Partial order reductions are aimed at alleviating
that problem. As an outcome of the work carried out for the
elaboration of current thesis, two new static partial order
techniques, named Na\"{i}ve SPOR and Reachability-Aware SPOR, were
defined. A recommendation of the situations in which each of them
should be used is provided. The latter achieves a better reduction
than the former when the system to be verified is not probabilistic or
when the property to be checked can be expressed in a linear temporal
logic. The software tool known as LiQuor model checker was extended in
order to be able to execute both reduction techniques. Those
techniques were utilized for the reduction of the models of some
classical concurrent systems. Several properties of the reduced and
unreduced models were verified using symbolic and explicit model
checking techniques. As a result of the analysis over the experiments,
it is concluded that static partial order techniques should be more
conveniently used in combination with symbolic model checking than
with explicit model checking.}
}
@mastersthesis{2011:phoenix,
  author = {Jingwei, Lu},
  title = {Extending Fuzzy Logic with characteristics Similarity and Quantification},
  school = {Facultad de Inform{\'a}tica, Universidad Polit{\'e}cnica de Madrid},
  year = {2011},
  month = {February},
  day = {11},
  url = {http://www.emcl-study.eu/graduates.html},
  internacional = {yes},
  note = {Advisors: Susana Mu{\~n}oz Hern{\'a}ndez and V{\'i}ctor Pablos Ceruelo, Calificaci{\'{o}}n: Sobresaliente (10/10)}
}
@mastersthesis{silva2011,
  author = {Nu{\~{n}}ez Silva, Diego},
  title = {Design and Implementation of a Media Access Component at {Picsearch} Using a Rigorous Software Engineering Approach},
  school = {Facultad de Inform{\'{a}}tica, Universidad Polit{\'{e}}cnica de Madrid},
  year = 2011,
  month = {November 2011},
  note = {Advisor: Lars-{\AA}ke Fredlund. Joint degree with Blekinge Institute of Technology, Sweden.}
}
@mastersthesis{avramovic2011,
  author = {Slavisa Avramovic},
  title = {Design and Implementation of a Servlet and Mobile Client for
Adaptive Location-Based Information Retrieval},
  school = {Facultad de Inform{\'{a}}tica, Universidad Polit{\'{e}}cnica de Madrid},
  year = 2011,
  month = {November 2011},
  note = {Advisor: Lars-{\AA}ke Fredlund. Joint degree with Technische Universit{\"at} Kaiserslautern, Germany.}
}
@inproceedings{2011:hema:slpoofs,
  tipoactividad = {Ponencias en congresos},
  internacional = {yes},
  author = {{{\'{A}}ngel} Herranz and Julio Mari{\~{n}}o},
  title = {Synthesis of Logic Programs from Object-Oriented Formal Specifications},
  booktitle = {Technical Communications of the 27th Int'l. Conference on Logic Programming (ICLP'11)},
  month = jul,
  year = 2011,
  pages = {95-105},
  editor = {John P. Gallagher and Michael Gelfond},
  url = {http://dx.doi.org/10.4230/LIPIcs.ICLP.2011.95},
  doi = {10.4230/LIPIcs.ICLP.2011.95},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume = {11},
  isbn = {978-3-939897-31-6},
  issn = {1868-8969},
  address = {Dagstuhl, Germany}
}
@inproceedings{2011:hebemama:mvernp,
  author = {{{\'{A}}ngel} Herranz and Clara Benac and Guillem Marpons and Julio Mari{\~{n}}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},
  addresss = {Lille, France}
}
@inproceedings{2011:GPN:TPF,
  tipoactividad = {Ponencias en congresos},
  internacional = {no},
  revisores = {yes},
  author = {{{\'{A}}lvaro} {Garc{\'{i}}a-P{\'{e}}rez} and Pablo Nogueira},
  title = {Estrategias del c{\'{a}}lculo lambda e interderivaci{\'{o}}n de
                  artefactos sem{\'{a}}nticos},
  booktitle = {Actas de las {XI} {J}ornadas sobre {P}rogramaci{\'{o}}n y
                  {L}enguajes - {PROLE}'11},
  url = {http://www.sistedes.es/ficheros/actas-conferencias/PROLE/2011.pdf},
  isbn = {978-84-9749-487-8},
  pages = {253--254},
  year = {2011},
  editor = {P. Arenas and V. M. Gul{\'{i}}as and P. Nogueira},
  address = {A Coru{\~{n}}a},
  month = sep,
  organization = {Sistedes},
  publisher = {Universidade da Coru{\~{n}}a},
  abstract = {En esta charla discutimos la relaci{\'{o}}n entre distintos
                  artefactos sem{\'{a}}nticos del c{\'{a}}lculo lambda, poniendo especial
                  atenci{\'{o}}n en una estrategia normalizante en el c{\'{a}}lculo lambda
                  value de Plotkin, a la que llamamos strict normal order.}
}
@unpublished{agp-imdea2011,
  tipoactividad = {Cursos, seminarios y tutoriales},
  internacional = {yes},
  author = {{{\'{A}}lvaro} {Garc{\'{i}}a-P{\'{e}}rez}},
  title = {Full Reduction in Open Strict Calculus},
  note = {Talk at {IMDEA} Software, Theory Lunch},
  revisores = {no},
  abstract = {Theorem provers based on dependent types rely on efficient
                  full-reducers implementing a beta-equivalence tester for
                  their typing rules. We present a full-reducing strategy in a
                  strict calculus allowing open terms. We traverse a path,
                  starting at weak-reduction in a non-strict calculus
                  restricted to closed terms (call-by-name). By successively
                  strengthening the congruence rules (reducing under lambda
                  abstractions), assuring normalisation (resorting to hybrid
                  strategies to find a normal form, if it exists), restricting
                  the notion of reduction (allowing only values as arguments)
                  and generalising the set of legal terms (including open
                  terms) we get a normalising strategy in Plotkin's lambda_V
                  theory. We show how these four different aspects
                  (strengthening congruence, normalisation, by-value semantics
                  and open terms) are entangled in this
                  traversal. Meta-theoretic issues regarding standardisation
                  and confluence lead the way to full-reduction.},
  organization = {The {IMDEA} Software Institute, Spain},
  address = {Montegancedo Science and Technology Park, Madrid, Spain},
  month = {May 24},
  year = {2011},
  pdf = {http://babel.ls.fi.upm.es/~agarcia/talks/Theory_lunch_2011_05_24/presentation.pdf}
}
@unpublished{gm-imdea2011,
  tipoactividad = {Cursos, seminarios y tutoriales},
  internacional = {yes},
  author = {Guillem Marpons},
  title = {Layered Coding Rule Definition and Enforcing Using
                  {LLVM}},
  note = {Talk at {IMDEA} Software, Theory Lunch},
  revisores = {no},
  abstract = {Coding rules are used in industry to enforce good
                  software practices that improve software reliability
                  and maintainability. Some examples of standard rule
                  sets are {MISRA-C/C++} and High Integrity C++.  In a
                  previous work we developed a framework to formalize
                  coding rules as logic programs, that can be later
                  run on a knowledge base of the program to
                  inspect. In order to formalize all the rules in
                  standard sets the knowledge base needs to contain
                  information about the program that ranges from
                  syntactic to undecidable semantic properties. As
                  many of the complex properties that coding rules
                  depend upon (or approximations to them) are computed
                  by static analyzers present in the literature, we
                  aim at reusing them presenting their result in a
                  uniform way that can be easily understood and
                  combined by engineers responsible for defining new
                  rules. In fact, some of those analyzes are
                  implemented in modern compilers, but their results
                  are almost exclusively applied to optimization.  In
                  this talk we present initial work on trying to use
                  the {LLVM} compiling infrastructure (http://llvm.org)
                  for enriching our program facts base with pointer
                  aliasing information, and how this information can
                  be used to define and enforce actual coding rules.},
  organization = {The {IMDEA} Software Institute, Spain},
  address = {Montegancedo Science and Technology Park, Madrid, Spain},
  month = {April 26},
  year = 2011,
  pdf = {http://babel.ls.fi.upm.es/~gmarpons/pubs/IMDEAtheoryLunch2011LayeredAnalysis.pdf}
}
@unpublished{agp-copenhagen,
  tipoactividad = {Cursos, seminarios y tutoriales},
  internacional = {yes},
  author = {{{\'{A}}lvaro} {Garc{\'{i}}a-P{\'{e}}rez}},
  title = {The Beta Cube},
  note = {Talk at the Programming, Logic and Semantics Group},
  descripcion = {Pure lambda calculus reduction strategies have been
                  thoroughly studied, as they constitute the foundations of
                  evaluation in many programming languages. Sestoft collected
                  and defined several of them as sets of big-step rules, thus
                  clarifying varying and inaccurate definitions in the
                  literature. From Sestoft's work, we present a rule template
                  which can instantiate any of the foremost strategies and
                  some more. Abstracting the parameters of the template, we
                  propose a space of reduction strategies we like to call the
                  Beta Cube. We also formalise a hybridisation
                  operator---informally suggested by Sestoft---which produces
                  new strategies by composing a subsidiary and a base strategy
                  from the cube. Furthermore, we discuss a variant of the
                  hybridisation operator, in which the operand of an
                  application is reduced by the subsidiary instead of the
                  hybrid. This accomplish with the implicit remarks on
                  Plotkin's theorems for the lambda-value calculus. The new
                  hybridisation operator allows to produce a normalising
                  strategy in Plotkin's (pure) lambda-value calculus. This
                  space gives new and interesting insights about the
                  properties of reduction strategies. We present and prove the
                  Absorption Theorem, which states that subsidiaries are
                  left-identities of their hybrids.},
  organization = {IT University, Copenhagen, {DK}},
  month = {March 7},
  year = {2011},
  pdf = {http://babel.ls.fi.upm.es/~agarcia/talks/ITU_beta_cube/presentation.pdf}
}
@unpublished{agp-aarhus,
  tipoactividad = {Cursos, seminarios y tutoriales},
  internacional = {yes},
  author = {{{\'{A}}lvaro} {Garc{\'{i}}a-P{\'{e}}rez}},
  title = {The Beta Cube},
  note = {Talk at the weakly PL Entropy Meeting},
  descripcion = {Pure lambda calculus reduction strategies have been
                  thoroughly studied, as they constitute the foundations of
                  evaluation in many programming languages. Sestoft collected
                  and defined several of them as sets of big-step rules, thus
                  clarifying varying and inaccurate definitions in the
                  literature. From Sestoft's work, we present a rule template
                  which can instantiate any of the foremost strategies and
                  some more. Abstracting the parameters of the template, we
                  propose a space of reduction strategies we like to call the
                  Beta Cube. We also formalise a hybridisation
                  operator---informally suggested by Sestoft---which produces
                  new strategies by composing a subsidiary and a base strategy
                  from the cube. Furthermore, we discuss a variant of the
                  hybridisation operator, in which the operand of an
                  application is reduced by the subsidiary instead of the
                  hybrid. This accomplish with the implicit remarks on
                  Plotkin's theorems for the lambda-value calculus. The new
                  hybridisation operator allows to produce a normalising
                  strategy in Plotkin's (pure) lambda-value calculus. This
                  space gives new and interesting insights about the
                  properties of reduction strategies. We present and prove the
                  Absorption Theorem, which states that subsidiaries are
                  left-identities of their hybrids.},
  url = {http://users-cs.au.dk/entropy-meetings/index.php/Feb_03_2011},
  organization = {Faculty of Science, Aarhus University, {DK}},
  month = {February 3},
  year = {2011}
}
@phdthesis{aherranz:thesis,
  author = {{{\'{A}}ngel} Herranz},
  title = {An Object-Oriented Formal Notation: Executable Specifications in Clay},
  school = {Universidad Polit{\'{e}}cnica de Madrid},
  year = {2011},
  month = jan
}
@article{castro_benac_fredlund_gulias_rivas:entcs2011,
  author = {D. Castro and C. Benac Earle and L. Fredlund and V. Gul{\'{i}}as and S. Rivas},
  title = {A Case Study on Verifying a Supervisor Component Using {McErlang}},
  journal = {ENTCS},
  volume = 271,
  year = 2011,
  month = {March},
  pages = {23-40},
  internacional = {yes},
  tipoactividad = {Art{\'{i}}culos en revistas},
  doi = {http://dx.doi.org/10.1016/j.entcs.2011.02.009},
  abstract = {In this paper we present a work in progress on the formal verification of a process supervisor using the McErlang model checker. The process supervisor is an alternative implementation of the standard supervisor behaviour of Erlang/OTP. This implementation, currently employed at the company LambdaStream, was checked against several safety and liveness properties.},
  issn = {1571-0661}
}
@inproceedings{cmmse11:2011:vpc-susana,
  author = {Pablos-Ceruelo, V{\'{i}}ctor and Mu{\~{n}}oz-Hern{\'{a}}ndez, Susana},
  booktitle = {CMMSE 2011 : Proceedings of the 11th International Conference on Mathematical Methods in Science and Engineering},
  title = {Introducing priorities in RFuzzy: Syntax and Semantics},
  day = {26-30},
  month = {June},
  year = {2011},
  address = {Benidorm (Alicante), Spain},
  optabstract = {},
  volume = {3},
  pages = {918-929},
  isbn = {978-84-614-6167-7},
  url = {http://gsii.usal.es/~CMMSE/index.php?option=com_content{\&}task=view{\&}id=15{\&}Itemid=16}
}
@article{MunozHernandez2011,
  title = {RFuzzy: Syntax, Semantics and Implementation Details of a Simple and Expressive Fuzzy Tool over Prolog},
  journal = {Information Sciences},
  volume = {181},
  number = {10},
  pages = {1951 - 1970},
  year = {2011},
  note = {Special Issue on Information Engineering Applications Based on Lattices},
  issn = {0020-0255},
  doi = {10.1016/j.ins.2010.07.033},
  url = {http://www.sciencedirect.com/science/article/B6V0C-50PJWYR-2/2/26d8ff890f0effc98aa1c12225a5fb87},
  author = {Mu{\~{n}}oz-Hern{\'{a}}ndez, Susana and Pablos-Ceruelo, V{\'{i}}ctor and Hannes {Strass}},
  keywords = {Fuzzy Logic, Logic Programming Application, Knowledge Representation and Reasoning, Semantics, Implementation},
  abstract = {We present the RFuzzy framework, a Prolog-based tool for representing and reasoning with fuzzy information. The advantages of our framework in comparison to previous tools along this line of research are its easy, user-friendly syntax, and its expressivity through the availability of default values and types. In this approach we describe the formal syntax, the operational semantics and the declarative semantics of RFuzzy (based on a lattice). A least model semantics, a least fixpoint semantics and an operational semantics are introduced and their equivalence is proven. We provide a real implementation that is free and available. (It can be downloaded from http://babel.ls.fi.upm.es/software/rfuzzy/.) Besides implementation details, we also discuss some actual applications using RFuzzy.}
}
@article{2011jigpal,
  tipoactividad = {Art{\'{i}}culos en revistas},
  internacional = {yes},
  author = {Emilio Jes{\'{u}}s {Gallego Arias} and James Lipton and Julio
                  Mari{\~{n}}o and Pablo Nogueira},
  title = {First-order Unification using Variable-Free Relational
                  Algebra},
  volume = {19},
  number = {6},
  pages = {790--820},
  year = {2011},
  issn = {1367-0751},
  doi = {10.1093/jigpal/jzq011},
  url = {http://jigpal.oxfordjournals.org/content/19/6/790.abstract},
  journal = {Logic Journal of IGPL},
  abstract = {We present a framework for the representation and resolution
                  of first-order unification problems and their abstract
                  syntax in a variable-free relational formalism which is an
                  executable variant of the Tarski-Givant relation algebra and
                  of Freyd's allegories restricted to the fragment necessary
                  to compile and run logic programs. We develop a decision
                  procedure for validity of relational terms, which
                  corresponds to solving the original unification problem. The
                  decision procedure is carried out by a conditional
                  relational-term rewriting system. There are advantages over
                  classical unification approaches. First, cumbersome and
                  underspecified meta-logical procedures (name clashes,
                  substitution, etc.)  and their properties (invariance under
                  substitution of ground terms, equality's congruence with
                  respect to term forming, etc.) are captured algebraically
                  within the framework. Second, other unification problems can
                  be accommodated, for example, existential quantification in
                  the logic can be interpreted as a new operation whose effect
                  is to formalize the costly and error prone handling of fresh
                  names (renaming apart).},
  publisher = {Oxford University Press}
}

This file was generated by bibtex2html 1.98.