@comment{{Al final apareció en 2018}}
@comment{{2015}}
@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.