Diego Nuñez Silva. Design and implementation of a media access component at Picsearch using a rigorous software engineering approach. Master's thesis, Facultad de Informática, Universidad Politécnica de Madrid, November 2011 2011. Advisor: Lars-Åke Fredlund. Joint degree with Blekinge Institute of Technology, Sweden. [ bib ]
Slavisa Avramovic. Design and implementation of a servlet and mobile client for adaptive location-based information retrieval. Master's thesis, Facultad de Informática, Universidad Politécnica de Madrid, November 2011 2011. Advisor: Lars-Åke Fredlund. Joint degree with Technische Universität Kaiserslautern, Germany. [ bib ]
Lars-Åke Fredlund. McErlang. Tutorial talk at the Erlang User Conference 2011, November 4 2011. [ bib | http ]
Lars-Åke Fredlund. Erlang QuickCheck and Java. Tutorial talk at the Erlang User Conference 2011, November 4 2011. [ bib | http ]
Purificación Arenas, Victor M. Gulías, and Pablo Nogueira, editors. Actas de las XI Jornadas sobre Programación y Lenguajes - PROLE'11. Universidade da Coruña, September 5--7 2011. [ bib | .pdf ]
Actas del congreso

Ana María Fernández-Soriano, Julio Mariño, and Ángel Herranz. A tool for the integration of constraint logic programming in spreadsheets. In Purificación Arenas, Víctor M. Gulías, and Pablo Nogueira, editors, Actas XI Jornadas sobre Programación y Lenguajes, pages 243--252, A Coruña, Spain, September 2011. ISBN 978-84-9749-487-8. [ bib ]
Álvaro García-Pérez and Pablo Nogueira. Estrategias del cálculo lambda e interderivación de artefactos semánticos. In P. Arenas, V. M. Gulías, and P. Nogueira, editors, Actas de las XI Jornadas sobre Programación y Lenguajes - PROLE'11, pages 253--254, A Coruña, September 2011. Sistedes, Universidade da Coruña. [ bib | .pdf ]
En esta charla discutimos la relación entre distintos artefactos semánticos del cálculo lambda, poniendo especial atención en una estrategia normalizante en el cálculo lambda value de Plotkin, a la que llamamos strict normal order.

Álvaro Fernández Díaz. Static partial order reduction for probabilistic systems. Master's thesis, Fakultät für Informatik, Technische Universität Dresden, July 29 2011. Advisor: Christel Baier, Calificación: Sobresaliente. [ bib | .html | .pdf ]
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ï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.

Miguel Ángel Polo Mancera. Polimorfismo ad-hoc en un lenguaje lógico funcional. Master's thesis, Facultad de Informática, Universidad Politécnica de Madrid, July 2011. Supervised by Julio Mariño (in Spanish). [ bib ]
Ángel Herranz and Julio Mariño. Synthesis of logic programs from object-oriented formal specifications. In John P. Gallagher and Michael Gelfond, editors, Technical Communications of the 27th Int'l. Conference on Logic Programming (ICLP'11), volume 11 of Leibniz International Proceedings in Informatics (LIPIcs), pages 95--105, Dagstuhl, Germany, July 2011. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | http ]
Víctor Pablos-Ceruelo and Susana Muñoz-Hernández. Introducing priorities in rfuzzy: Syntax and semantics. In CMMSE 2011 : Proceedings of the 11th International Conference on Mathematical Methods in Science and Engineering, volume 3, pages 918--929, Benidorm (Alicante), Spain, June 2011. [ bib | http ]
Álvaro García-Pérez. Full reduction in open strict calculus. Talk at IMDEA Software, Theory Lunch, May 24 2011. [ bib | .pdf ]
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.

Ángel Herranz, Clara Benac, Guillem Marpons, and Julio Mariño. Mechanising the validation of ERTMS requirements and new procedures. In 9th World Congress on Railway Research, page 33, May 2011. [ bib | .pdf ]
Guillem Marpons. Layered coding rule definition and enforcing using LLVM. Talk at IMDEA Software, Theory Lunch, April 26 2011. [ bib | .pdf ]
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.

Álvaro García-Pérez. The beta cube. Talk at the Programming, Logic and Semantics Group, March 7 2011. [ bib | .pdf ]
D. Castro, C. Benac Earle, L. Fredlund, V. Gulías, and S. Rivas. A case study on verifying a supervisor component using McErlang. ENTCS, 271:23--40, March 2011. [ bib | DOI ]
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.

Álvaro García-Pérez. The beta cube. Talk at the weakly PL Entropy Meeting, February 3 2011. [ bib | http ]
Lu Jingwei. Extending fuzzy logic with characteristics similarity and quantification. Master's thesis, Facultad de Informática, Universidad Politécnica de Madrid, February 2011. Advisors: Susana Muñoz Hernández and Víctor Pablos Ceruelo, Calificación: Sobresaliente (10/10). [ bib | .html ]
Julio Mariño, editor. Functional and Constraint Logic Programming, 19th International Workshop, Revised Selected Papers, volume 6559 of LNCS. Springer Verlag, 2011. [ bib ]
Álvaro Fernández-Díaz, Clara Benac, and Lars-Åke Fredlund. Erlang implementation and formal verification of a distributed MAS protocol. In Nogueira, Arenas, and Gulías, editors, XI Jornadas sobre Programación y Lenguajes, PROLE2011. Universidades da Coruña, 2011. [ bib ]
Murdoch J. Gabbay. Festschrift in honour of Howard Barringer. chapter Stone Duality for First-order Logic: a Nominal Approach to Logic and Topology. 2011. [ bib ]
Ángel Herranz and Julio Mariño. A verified implementation of priority monitors in Java. In Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov, editors, Papers presented at the 2nd. International Conference on Formal Verification of Object-Oriented Software (FoVeOOS'11), number 26, pages 244--259, Turin, Italy, 2011. Karlsruhe Reports in Informatics. ISSN 2190-4782. [ bib ]
Ángel Herranz. An Object-Oriented Formal Notation: Executable Specifications in Clay. PhD thesis, Universidad Politécnica de Madrid, January 2011. [ bib ]
Susana Muñoz-Hernández, Víctor Pablos-Ceruelo, and Hannes Strass. Rfuzzy: Syntax, semantics and implementation details of a simple and expressive fuzzy tool over prolog. Information Sciences, 181(10):1951 -- 1970, 2011. Special Issue on Information Engineering Applications Based on Lattices. [ bib | DOI | http ]
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.

Keywords: Fuzzy Logic, Logic Programming Application, Knowledge Representation and Reasoning, Semantics, Implementation
Emilio Jesús Gallego Arias, James Lipton, Julio Mariño, and Pablo Nogueira. First-order unification using variable-free relational algebra. Logic Journal of IGPL, 19(6):790--820, 2011. [ bib | DOI | http ]
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).

This file was generated by bibtex2html 1.98.