PROGRAMMING THEORY

Author: CALATAYUD RAMOS AYMEE.
Year: 2003.
University: POLITÉCNICA DE MADRID [www.upm.es].
Place of defense: FACULTAD DE INFORMÁTICA.
Place of preparation: FACULTAD DE INFORMÁTICA.

Summary: In this report we study problems related to the geometrical Location Services. The Location Services deals with the placement of one or more resources (radars, warehouses, oil explorers wells, etc.). Way to optimize certain goals (serve the greatest number of users possible, minimize the cost of transportation, avoid pollution from nearby towns, etc..). The resolution of such problems in real life leads to very interesting geometric problems. The geometric approach of some potential users of the service are represented by dots while services are represented by the geometrical figure best suited to service: a ring in the case of radar, radio and television antennae, aspesores, etc., a wedge if the service we want to provide is lighting, for example. These are the geometric figures with which we worked. In our case the service will be only one and the formal approach to the problem is as follows: given a ring or a wedge of fixed size and a set of n points on the plane, finding what must be the position of the same to be filled the largest number of points. To solve these problems we used arrangements of curves in the plane. The arrangements are a geometric structure well known and studied within the Computational Geometry. We have focused on arrangements curves bounded Jordan not to be cut two to two at most two points, as these were the arrangements with which we have had to deal with for resolving the problems. Among the different techniques for building arrangements, we have studied the incremental method, as it leads to simpler algorithms from the point of view of consolidation. As a result of this study we have achieved new heights of complexity that improve the time to build these arrangements with incremental algorithms. The new peak O (nlambda3 (n)) represents an improvement over the peak known so far: O (nlambda4 (n)). We have also seen that under certain conditions these arrangements can be made in time O (nlambda2 (n)), which is the optimum height for the construction of these arrangements. Restricting the study to specific curves, we got that arrangements No circumferences of k different radii can be built in time O (n2 min (log (K), alpha (n))), a result that also applies to arrangements ellipses, parabolas or hyperbolas of different sizes when the figures are all isotéticas.

Author: PALOMINO TARJUELO MIGUEL.
Year: 2004.
University: COMPLUTENSE DE MADRID [www.ucm.es].
Place of defense: FACULTAD DE CIENCIAS MATEMÁTICAS.
Place of preparation: FACULTAD DE CIENCIAS MATEMÁTICAS.

Summary: The rewrite is a logical extension of the usual logic ecuacional which was introduced as a model parala specification of concurrent systems that unifies many previous proposals. Since then, this logic has proved to be a formality very flexible, not only for the specification of the competition, but also as semantic and logical framework in which to interpret other logical and computer models. Since its introduction, was filed logic as the basis of a declarative language specification and programming, called Maude. The study of the mathematical properties of logic rewrite is necessary to justify its use as a tool for design and specification. One of these properties, of paramount importance in this logic, it is thought that intuitively is the ability of a computer system or logical access to their own metanivel to control their behavior. In this thesis we give a detailed demonstration of the reflectivity of logic rewrite that extends previous work on more restricted versions of logic. In addition, we present a unifying approach, drawing on previous work for the study of the thinking in some sublógicas of logic as are rewriting logic belonging to the logic of equal horn. The reflection on the logic rewrite it also has a practical side clearly that proposed the use of reflection for metarrozanamiento formal. In this thesis is progressing in these ideas, generalizing inductive principles proposed by other authors and exploring how to apply to demonstrate semantic relations between theories on the logic of belonging. The other major topic of the thesis is the search for methods of demonstration for the verification of systems with specified therein. For verifying properties in rewriting system, starting with its version 2.0 system Maude includes a model checker. The technical verification of models has emerged as one of the happiest stories in the field of application of formal methods to validate properties at the industrial system. Despite this, the inherent limitation of the testers models for dealing infinite systems, or simply too large, has led many researchers to study techniques of abstraction to overcome that. Our interest in this area lies in the study of how to apply the techniques of abstraction within the logic of rewriting. On the one hand, we are interested in exploring possible generalizations of the ideas of abstraction and simulation within a categorical more abstract than in the regularly scheduled. For another, how to define those abstractions in rewriting logic and Maude. For this we extend the usual notion of simulation in three directions and show how it may represent the level of the logic of rewriting through subsequent generalizations. He also presented a study of the basic properties of the categories that give rise to these simulations. Lastly, we developed a prototype in Maude which automates the process of abstraction, in particular, the process of abstraction preachers. Its design is thoughtful and makes use of key ITP, a demonstrator developed theorems on Madude, which serves as an oracle able to decide the validity of the numerous ways depending on which system is built abstract.

Author: Sanchez Penas Juan Jose.
Year: 2006.
University: A CORUÑA [www.udc.es].
Place of defense: Facultad de Informática.
Place of preparation: Facultad de Informática.

Summary: The thesis looks like going from the software architecture to formal verification of a distributed system. As motivation and case study research, we use a video on demand server developed by our research group. The software architecture of this system is very flexible and complex, and better tools are needed to improve the quality of the system. The thesis explores how to use formal methods for that. Using various tools of the area, we propose an innovative method for automatically extracting information about performance. As input, we use the source code and system configuration, as output, information on performance and bottlenecks. It demonstrates the method with the video servers and generalizes to other tools and systems.