@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.*