[MH10g]
Susana Muñoz-Hernández. Seminario "introducción al trabajo en equipo ii". II Plan de Tutoría Curricular de la Facultad de Informática de la Universidad Politécnica de Madrid, October 19 2010. [ bib | .pdf ]
[FCL10]
Álvaro Fernández Díaz, Clara Benac Earle, and Lars-Åke Fredlund. Implementing a multiagent negotiation protocol in erlang. In Ninth ACM SIGPLAN Erlang Workshop, Erlang'10, pages 69--74, Baltimore, Maryland, USA, September 30 2010. ACM. [ bib | .pdf ]
In this paper we present the verification of a multi-agent negotiation protocol. The verification of this kind of highly concurrent and distributed systems is hard. We present some evidence that shows Erlang is a very good choice for implementing this kind of systems due to the quite high mapping between the protocol specification and Erlang constructs. The use of this programming language also provides the capability to handle a larger number of agents than other implementations, with substantially better performance.

[Gar10b]
Álvaro García-Pérez. El cubo beta. Charla impartida en el II Taller de Programación Funcional TPF 2010, September 7 2010. [ bib | http ]
[PCFMH10]
Víctor Pablos-Ceruelo, Álvaro Fernández Díaz, and Susana Muñoz-Hernández. Developing user-sensitive search engines from fuzzy concepts. In Actas XV Jornadas de Ingeniería del Software y Bases de Datos (JISBD'10), pages 175--186, Valencia, Spain, September 7-10 2010. http://www.dsic.upv.es/conferences/jisbd2010/articulos.shtml. [ bib ]
[Nog10]
Pablo Nogueira. Programación genérica funcional: variaciones sobre los mismos temas. In II Taller de Programación Funcional, X Jornadas sobre Programación y Lenguajes - PROLE'10, III Congreso Español de Informática - CEDI'10, Valencia, September 7 2010. Sociedad Científica Informática de España, IEEE Sección España, Universidad Politécnica de Valencia. [ bib ]
[MH10d]
Susana Muñoz-Hernández. Mesa redonda "?`qué hace la universidad por el acercamiento de las culturas?". VII Jornadas Internacionales de Innovación Universitaria de la Universidad Europea de Madrid, September 6 2010. [ bib ]
[MH10f]
Susana Muñoz-Hernández. Seminario "introducción al trabajo en equipo i". II Plan de Tutoría Curricular de la Facultad de Informática de la Universidad Politécnica de Madrid, September 2 2010. [ bib | .pdf ]
[SEF10]
H. Svensson, C. Benac Earle, and L. Fredlund. A unified semantics for future erlang. In Ninth ACM SIGPLAN Erlang Workshop, Erlang'10, pages 23--32, Baltimore, Maryland, USA, September 2010. ACM. [ bib | .pdf ]
[CEF+10b]
D. Castro, C. Benac Earle, L. Fredlund, V. Gulías, and S. Rivas. A verification of a process supervisor with mcerlang. In PROLE 2010 -- Jornadas sobre Programacion y Lenguajes, September 2010. [ bib | .pdf ]
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, in use at the company LambdaStream, was checked against several safety and liveness properties.

[MH10c]
Susana Muñoz Hernández. Internacionalización en los estudios de máster. 1a Jornada De Innovación Educativa: Innovación en la gestión y organización de la docencia y del aprendizaje en los títulos de grado y máster, July 14 2010. [ bib | .pdf ]
[GNG10]
Álvaro García, Pablo Nogueira, and Emilio Jesús Gallego Arias. The beta cube (extended abstract). In César Muñoz and Hélène Kirchner, editors, Proceedings of the 1st International Workshop on Strategies in Rewriting, Proving, and Programming - IWS'10, pages 3--7, Edinburgh, UK, July 9 2010. [ bib | .pdf | .pdf ]
We define a big-step-style template for reduction strategies that can be instantiated to the foremost (and more) reduction strategies of the pure lambda calculus. We implement the template in Haskell as a parametric monadic reducer whose fixed points are reduction strategies. The resulting code is clean and abstracts away from the machinery required to guarantee semantics preservation for all strategies in lazy Haskell. By interpreting some parameters as boolean switches we obtain a reduction strategy lattice or beta cube which captures the strategy space neatly and systematically. We define a hybridisation function that generates hybrid strategies by composing a base and a subsidiary strategy from the cube. We prove an absorption theorem which states that subsidiaries are left-identities of their hybrids. More properties from the cube remain to be explored

[MH10i]
Susana Muñoz Hernández. Tecnología para el desarrollo y la cooperación: visión crítica. Introducción a la cooperación universitaria para el desarrollo, July 7 2010. [ bib ]
[MMMPR10]
Jesús Martínez-Mateo, Susana Muñoz-Hernández, and David Pérez-Rey. A Discussion of Thin Client Technology for Computer Labs. In Boris Shishkov, George A. Tsihrintzis, and Maria Virvou, editors, First International Multi-Conference on Innovative Developments in ICT (INNOV 2010), pages 119--124. Interdisciplinary Institute for Collaboration and Research on Enterprise Systems and Technology (IICREST), July 2010. First International Conference on Technology-Enhanced Learning (ICTEL 2010). [ bib ]
[HM10]
Ángel Herranz and Julio Mariño. Executable specifications in an object oriented formal notation. In 20th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2010, pages 144--158, Hagenberg, Austria, July 2010. Research Institute for Symbolic Computation (RISC) of the Johannes Kepler University Linz. [ bib | .pdf ]
Early validation of requirements is crucial for the rigorous development of software. Without it, even the most formal of the methodologies will produce the wrong outcome. One successful approach, popularised by some of the so-called lightweight formal methods, consists in generating (finite, small) models of the specifications. Another possibility is to build a running prototype from those specifications. In this paper we show how to obtain executable prototypes from formal specifications written in an object oriented notation by translating them into logic programs. This has a number of advantages over other lightweight methodologies. For instance, we recover the possibility of dealing with recursive data types as specifications that use them often lack finite models.

[CEF+10a]
D. Castro, C. Benac Earle, L. Fredlund, V. Gulías, and S. Rivas. Using McErlang to verify an Erlang process supervision component. In Trends in Functional Programming 2010, May 2010. [ bib | .pdf ]
We present a case-study in which a tool for model checking programs written in Erlang, McErlang, was used to verify a complex concurrent component. The component is an alternative implementation of the standard supervisor behaviour of Erlang/OTP. This implementation, in use at the company LambdaStream, was checked against several safety and liveness properties. In one case, McErlang found an error.

[MH10b]
Susana Muñoz Hernández. Experiéncias de tic en desarrollo. Ingeniería de Telecomunicación en Cooperación para el Desarrollo, April 29 2010. [ bib | .pdf ]
[MH10h]
Susana Muñoz Hernández. Tecnologia para el desarrollo y la cooperacion (tedeco). 1a Jornada de Solidaridad y Cooperacion de la UPM, April 28 2010. [ bib | .pdf ]
[FMHPC10]
Álvaro Fernández Díaz, Susana Muñoz-Hernández, and Víctor Pablos-Ceruelo. Developing user-sensitive e-commerce applications from fuzzy concepts. In Algebraic methods, soft computing, and program verification, "International Center for Mathematical Meetings (CIEM), Castro Urdiales (Cantabria), Spain", April 21-23 2010. Julio Rubio (Univ. de La Rioja) and Manuel Ojeda-Aciego (Univ. de Málaga). Sponsored by: Ingenio2010, CIEM, Excmo. Ayuntamiento de Castro Urdiales. Keynote Speakers: Thomas Arts (Univ. of Gothenburg), Gilles Barthe (Madrid Institute for Advanced Studies (Software)), Stefan Berghofer (Technische Universität München), Mario de Jesús Pérez Jiménez (Univ. de Sevilla), José Luis Ruiz Reina (Univ. de Sevilla), Enric Trillas (European Centre for Soft Computing). [ bib ]
[MdRM10]
J.M. Mateo, D.P. del Rey, and Susana Muñoz-Hernández. Student motivation and cross-curricular development through e-learning applied to cooperation. In Education Engineering (EDUCON), 2010 IEEE, pages 913 --920, April 2010. [ bib | DOI ]
Technologies and especially information and communication technologies (ICT) are barrier breaking in the current social scenario. Their use is becoming essential for any professional, and their scope of use is becoming particularly widespread in education due to the existence of communication outside the classroom through e-learning tools. Universities, which play an innovative role in education, are using ICT-based approaches to adapt their learning methodology. In this paper, we present a model where students from first-world universities prepare and adapt course contents for use in educational institutions in developing countries. The objectives of this initiative of students' participating in e-learning projects with developing countries are to improve their motivation, develop a set of cross-curricular competencies, and transfer technologies within the scope of university development cooperation.

Keywords: course contents;cross-curricular development;e-learning;educational institutions;educational universities;information and communication technologies;student motivation;university development cooperation;computer aided instruction;educational courses;educational institutions;
[Gar10a]
Álvaro García-Pérez. The beta cube, March 29 2010. Poster at the BRICS Retreat 2011. [ bib | .pdf ]
The Beta Cube systematises and articulates a plethora of lambda claculus reduction strategies. Along with the cube, we present an hybridisation operator, which allows to produce new strategies composing two existing strategies from the cube. The cube reveals interesting algebraic properties of the strategies and helps to reason about standardization and normalization regarding to different lambda theories.

[Mon10]
Rubén Monjaraz. From the π-calculus to Flat GHC. Master's thesis, Facultad de Informática, Universidad Politécnica de Madrid, March 2010. Advisor: Julio Mariño. Joint degree with TU Dresden. [ bib ]
[HP10a]
Ángel Herranz and Iván Pérez. Communication models for resource mashups. Technical Report UPM-BABEL-2010-002, Babel Group, Universidad Politécnica de Madrid, March 2010. [ bib ]
[GM10]
Murdoch J. Gabbay and Dominic Mulligan. Curry-howard for incomplete first-order logic derivations using one-and-a-half level terms. Information and Computation, 208:230--258, March 2010. [ bib | DOI ]
[MH10a]
Susana Muñoz Hernández. Emerging free software market in developing countries. SIGs Online SHARE Event, February 17 2010. [ bib | .pdf ]
[TdlVLGMH10b]
Teresa Trigo de la Vega, Pedro López-García, and Susana Muñoz-Hernández. Towards fuzzy granularity control in parallel/distributed computing. In Joaquim Filipe and Janusz Kacprzyk, editors, IJCCI (ICFC-ICNC), pages 43--55. SciTePress, 2010. Best Student Paper Award ICFC 2010. [ bib ]
[TdlVLGMH10a]
Teresa Trigo de la Vega, Pedro López-García, and Susana Muñoz-Hernández. A fuzzy approach to resource aware automatic parallelization. In Kurosh Madani, António Dourado Correia, Agostinho C. Rosa, and Joaquim Filipe, editors, Computational Intelligence - Revised and Selected Papers of the International Joint Conference, IJCCI 2010, Valencia, Spain, October 2010, volume 399 of Studies in Computational Intelligence, pages 229--245. Springer, 2010. [ bib | DOI | http ]
[MH10e]
Susana Muñoz-Hernández. Robot Soccer, chapter RFuzzy: an Easy and Expressive Tool for Modelling the Cognitive Layer in RoboCupSoccer. InTech, 2010. Editor Vladan Papic. [ bib | http ]
[HP10b]
Ángel Herranz and Iván Pérez. Compatible communication in mashups. Technical Report UPM-BABEL-2010-001, Babel Group, Universidad Politécnica de Madrid, January 2010. [ bib ]
[DWA+10]
John Derrick, Neil Walkinshaw, Thomas Arts, Clara Benac Earle, Francesco Cesarini, Lars-Ake Fredlund, Victor Gulias, John Hughes, and Simon Thompson. Property-based testing - the protest project. 6286:250--271, 2010. [ bib | http ]
[GDEF10]
Qiang Guo, John Derrick, Clara Benac Earle, and Lars-Åke Fredlund. Model-checking erlang - a comparison between etomcrl2 and mcerlang. In Testing - practice and research techniques (TAIC PART 2010), number 6303, pages 23--3. LNCS, Springer Verlag, 2010. [ bib ]
Model-checking programs is important in the development of a reliable software system. Two approaches might be applied to model-check a system at a source code level. One is to directly apply model-checking algorithm to the programming language; the other to abstract the program source codes into a formal specification, upon which some standard model-checkers can be used to verify system's properties. Both methods have recently been investigated for model-checking the functional programming language Erlang. Correspondingly, two Erlang model-checkers McErlang and Etomcrl2 are developed. This paper evaluates the two model-checkers by applying them to verify a a distributed and concurrent example - telecoms implemented in Erlang/OTP. A number of system key properties are model-checked with both tool-sets. Advantages and disadvantages upon the uses of Etomcrl2 and McErlang are compared and summarized. Through such a case study, we intend to evaluate the two model-checkers on their effectiveness when verifying distributed and concurrent systems, and propose suggestions for their future work.


This file was generated by bibtex2html 1.98.