A geometric characterization of the upper bound for the span of the jones polynomial

Let D be a link diagram with n crossings, sA and sB be its extreme states and |sAD| (respectively, |sBD|) be the number of simple closed curves that appear when smoothing D according to sA (respectively, sB). We give a general formula for the sum |sAD| + |sBD| for a k-almost alternating diagram D, for any k, characterizing this sum as the number of faces in an appropriate triangulation of an appropriate surface with boundary. When D is dealternator connected, the triangulation is especially simple, yielding |sAD| + |sBD| = n + 2 - 2k. This gives a simple geometric proof of the upper bound of the span of the Jones polynomial for dealternator connected diagrams, a result first obtained by Zhu [On Kauffman brackets, J. Knot Theory Ramifications6(1) (1997) 125–148.]. Another upper bound of the span of the Jones polynomial for dealternator connected and dealternator reduced diagrams, discovered historically first by Adams et al. [Almost alternating links, Topology Appl.46(2) (1992) 151–165.], is obtained as a corollary. As a new application, we prove that the Turaev genus is equal to the number k of dealternator crossings for any dealternator connected diagram

Estimating the computational cost of logic programs

Information about the computational cost of programs is potentially useful for a variety of purposes, including selecting among different algorithms, guiding program transformations, in granularity control and mapping decisions in parallelizing compilers, and query optimization in deductive databases. Cost analysis of logic programs is complicated by nondeterminism: on the one hand, procedures can return múltiple Solutions, making it necessary to estímate the number of solutions in order to give nontrivial upper bound cost estimates; on the other hand, the possibility of failure has to be taken into account while estimating lower bounds. Here we discuss techniques to address these problems to some extent.

Interval-based resource usage verification: Formalization and prototype

In an increasing number of applications (e.g., in embedded, real-time, or mobile systems) it is important or even essential to ensure conformance with respect to a specification expressing resource usages, such as execution time, memory, energy, or user-defined resources. In previous work we have presented a novel framework for data size-aware, static resource usage verification. Specifications can include both lower and upper bound resource usage functions. In order to statically check such specifications, both upper- and lower-bound resource usage functions (on input data sizes) approximating the actual resource usage of the program which are automatically inferred and compared against the specification. The outcome of the static checking of assertions can express intervals for the input data sizes such that a given specification can be proved for some intervals but disproved for others. After an overview of the approach in this paper we provide a number of novel contributions: we present a full formalization, and we report on and provide results from an implementation within the Ciao/CiaoPP framework (which provides a general, unified platform for static and run-time verification, as well as unit testing). We also generalize the checking of assertions to allow preconditions expressing intervals within which the input data size of a program is supposed to lie (i.e., intervals for which each assertion is applicable), and we extend the class of resource usage functions that can be checked.

User-definable resource usage bounds analysis for java bytecode

Automatic cost analysis of programs has been traditionally concentrated on a reduced number of resources such as execution steps, time, or memory. However, the increasing relevance of analysis applications such as static debugging and/or certiflcation of user-level properties (including for mobile code) makes it interesting to develop analyses for resource notions that are actually application-dependent. This may include, for example, bytes sent or received by an application, number of files left open, number of SMSs sent or received, number of accesses to a datábase, money spent, energy consumption, etc. We present a fully automated analysis for inferring upper bounds on the usage that a Java bytecode program makes of a set of application programmer-deflnable resources. In our context, a resource is defined by programmer-provided annotations which state the basic consumption that certain program elements make of that resource. From these deflnitions our analysis derives functions which return an upper bound on the usage that the whole program (and individual blocks) make of that resource for any given set of input data sizes. The analysis proposed is independent of the particular resource. We also present some experimental results from a prototype implementation of the approach covering a signiflcant set of interesting resources.

Customizable resource usage analysis for java bytecode

Automatic cost analysis of programs has been traditionally studied in terms of a number of concrete, predefined resources such as execution steps, time, or memory. However, the increasing relevance of analysis applications such as static debugging and/or certification of user-level properties (including for mobile code) makes it interesting to develop analyses for resource notions that are actually applicationdependent. This may include, for example, bytes sent or received by an application, number of files left open, number of SMSs sent or received, number of accesses to a database, money spent, energy consumption, etc. We present a fully automated analysis for inferring upper bounds on the usage that a Java bytecode program makes of a set of application programmer-definable resources. In our context, a resource is defined by programmer-provided annotations which state the basic consumption that certain program elements make of that resource. From these definitions our analysis derives functions which return an upper bound on the usage that the whole program (and individual blocks) make of that resource for any given set of input data sizes. The analysis proposed is independent of the particular resource. We also present some experimental results from a prototype implementation of the approach covering an ample set of interesting resources.

A generic, context sensitive analysis framework for object oriented programs

Abstract interpreters rely on the existence of a nxpoint algorithm that calculates a least upper bound approximation of the semantics of the program. Usually, that algorithm is described in terms of the particular language in study and therefore it is not directly applicable to programs written in a different source language. In this paper we introduce a generic, block-based, and uniform representation of the program control flow graph and a language-independent nxpoint algorithm that can be applied to a variety of languages and, in particular, Java. Two major characteristics of our approach are accuracy (obtained through a topdown, context sensitive approach) and reasonable efficiency (achieved by means of memoization and dependency tracking techniques). We have also implemented the proposed framework and show some initial experimental results for standard benchmarks, which further support the feasibility of the solution adopted.

The Minimum Number of Points Taking Part in k-Sets in Sets of Unaligned Points

En este trabajo se da un ejemplo de un conjunto de n puntos situados en posición general, en el que se alcanza el mínimo número de puntos que pueden formar parte de algún k-set para todo k con 1menor que=kmenor quen/2. Se generaliza también, a puntos en posición no general, el resultado de Erdõs et al., 1973, sobre el mínimo número de puntos que pueden formar parte de algún k-set. The study of k- sets is a very relevant topic in the research area of computational geometry. The study of the maximum and minimum number of k-sets in sets of points of the plane in general position, specifically, has been developed at great length in the literature. With respect to the maximum number of k-sets, lower bounds for this maximum have been provided by Erdõs et al., Edelsbrunner and Welzl, and later by Toth. Dey also stated an upper bound for this maximum number of k-sets. With respect to the minimum number of k-set, this has been stated by Erdos el al. and, independently, by Lovasz et al. In this paper the authors give an example of a set of n points in the plane in general position (no three collinear), in which the minimum number of points that can take part in, at least, a k-set is attained for every k with 1 ≤ k < n/2. The authors also extend Erdos’s result about the minimum number of points in general position which can take part in a k-set to a set of n points not necessarily in general position. That is why this work complements the classic works we have mentioned before.

Goal-oriented self-adaptive hp-strategies for finite element analysis of electromagnetic scattering and radiation problems

In this paper, a fully automatic goal-oriented hp-adaptive finite element strategy for open region electromagnetic problems (radiation and scattering) is presented. The methodology leads to exponential rates of convergence in terms of an upper bound of an user-prescribed quantity of interest. Thus, the adaptivity may be guided to provide an optimal error, not globally for the field in the whole finite element domain, but for specific parameters of engineering interest. For instance, the error on the numerical computation of the S-parameters of an antenna array, the field radiated by an antenna, or the Radar Cross Section on given directions, can be minimized. The efficiency of the approach is illustrated with several numerical simulations with two dimensional problem domains. Results include the comparison with the previously developed energy-norm based hp-adaptivity.

Implementing the weakest failure detector for solving consensus

The concept of unreliable failure detector was introduced by Chandra and Toueg as a mechanism that provides information about process failures. This mechanism has been used to solve several agreement problems, such as the consensus problem. In this paper, algorithms that implement failure detectors in partially synchronous systems are presented. First two simple algorithms of the weakest class to solve the consensus problem, namely the Eventually Strong class (⋄S), are presented. While the first algorithm is wait-free, the second algorithm is f-resilient, where f is a known upper bound on the number of faulty processes. Both algorithms guarantee that, eventually, all the correct processes agree permanently on a common correct process, i.e. they also implement a failure detector of the class Omega (Ω). They are also shown to be optimal in terms of the number of communication links used forever. Additionally, a wait-free algorithm that implements a failure detector of the Eventually Perfect class (⋄P) is presented. This algorithm is shown to be optimal in terms of the number of bidirectional links used forever.

Sensibilidad a las entallas del acero inoxidable dúplex fuertemente trefilado

En el presente trabajo se estudia la sensibilidad a las entallas suaves de alambres de acero inoxidable dúplex fuertemente trefilado. Las entallas consideradas son reducciones de la sección transversal del alambre no simétricas respecto al eje de revolución. Tras constatar experimentalmente que los alambres con este tipo de daño fallan por agotamiento plástico, se ha determinado numéricamente la carga de agotamiento plástico en función de la profundidad de entalla empleando un mode-lo computacional de elementos finitos. Los resultados numéricos indican que la mayor deformabilidad del alambre debida a la entalla actúa en favor de su tolerancia al daño y permite que ésta alcance el límite superior dado por la carga de agotamiento a tracción simple del ligamento resistente.This research deals with the sensitivity to blunt notches of highly cold-drawn wires made of dúplex stainless steel. The analyzed notches are actually reductions of the wire cross section, asymmetrically mechanized with respect to the longitudinal wire axis. Once experimentally verified that the notched wires fail by plástic collapse, the failure load was found as a function of notch depth by means of a finite element model. The numerical results show that the higher compliance of the wires provided by the notch increases their damage tolerance up to the upper bound given by the tensile plástic failure load of the notch ligament.

La estabilidad del frente de excavación de un túnel en terrenos heterogéneos o con un criterio de rotura no-lineal

El frente de un túnel puede colapsar si la presión aplicada sobre el es inferior a un valor limite denominado presión “critica” o “de colapso”. En este trabajo se desarrolla y presenta un mecanismo de rotura rotacional generado punto a punto para el cálculo de la presión de colapso del frente de túneles excavados en terrenos estratificados o en materiales que siguen un criterio de rotura nolineal. La solución propuesta es una solución de contorno superior en el marco del Análisis Límite y supone una generalización del mecanismo de rotura mas reciente existente en la bibliografía. La presencia de un terreno estratificado o con un criterio de rotura no-lineal implica una variabilidad espacial de las propiedades resistentes. Debido a esto, se generaliza el mecanismo desarrollado por Mollon et al. (2011b) para suelos, de tal forma que se puedan considerar valores locales del ángulo de rozamiento y de la cohesión. Además, la estratificación del terreno permite una rotura parcial del frente, por lo que se implementa esta posibilidad en el mecanismo, siendo la primera solución que emplea un mecanismo de rotura que se ajusta a la estratigrafía del terreno. Por otro lado, la presencia de un material con un criterio de rotura no-lineal exige introducir en el modelo, como variable de estudio, el estado tensional en el frente, el cual se somete al mismo proceso de optimización que las variables geométricas del mecanismo. Se emplea un modelo numérico 3D para validar las predicciones del mecanismo de Análisis Limite, demostrando que proporciona, con un esfuerzo computacional significativamente reducido, buenas predicciones de la presión critica, del tipo de rotura (global o parcial) en terrenos estratificados y de la geometría de fallo. El mecanismo validado se utiliza para realizar diferentes estudios paramétricos sobre la influencia de la estratigrafía en la presión de colapso. Igualmente, se emplea para elaborar cuadros de diseño de la presión de colapso para túneles ejecutados con tuneladora en macizos rocosos de mala calidad y para analizar la influencia en la estabilidad del frente del método constructivo. Asimismo, se lleva a cabo un estudio de fiabilidad de la estabilidad del frente de un túnel excavado en un macizo rocoso altamente fracturado. A partir de el se analiza como afectan las diferentes hipótesis acerca de los tipos de distribución y de las estructuras de correlación a los resultados de fiabilidad. Se investiga también la sensibilidad de los índices de fiabilidad a los cambios en las variables aleatorias, identificando las mas relevantes para el diseño. Por ultimo, se lleva a cabo un estudio experimental mediante un modelo de laboratorio a escala reducida. El modelo representa medio túnel, lo cual permite registrar el movimiento del material mediante una técnica de correlación de imágenes fotográficas. El ensayo se realiza con una arena seca y se controla por deformaciones mediante un pistón que simula el frente. Los resultados obtenidos se comparan con las estimaciones de la solución de Análisis Límite, obteniéndose un ajuste razonable, de acuerdo a la literatura, tanto en la geometría de rotura como en la presión de colapso. A tunnel face may collapse if the applied support pressure is lower than a limit value called the ‘critical’ or ‘collapse’ pressure. In this work, an advanced rotational failure mechanism generated ‘‘point-by-point” is developed to compute the collapse pressure for tunnel faces in layered (or stratified) grounds or in materials that follow a non-linear failure criterion. The proposed solution is an upper bound solution in the framework of limit analysis which extends the most advanced face failure mechanism in the literature. The excavation of the tunnel in a layered ground or in materials with a non-linear failure criterion may lead to a spatial variability of the strength properties. Because of this, the rotational mechanism recently proposed by Mollon et al. (2011b) for Mohr-Coulomb soils is generalized so that it can consider local values of the friction angle and of the cohesion. For layered soils, the mechanism needs to be extended to consider the possibility for partial collapse. The proposed methodology is the first solution with a partial collapse mechanism that can fit to the stratification. Similarly, the use of a nonlinear failure criterion introduces the need to introduce new parameters in the optimization problem to consider the distribution of normal stresses along the failure surface. A 3D numerical model is employed to validate the predictions of the limit analysis mechanism, demonstrating that it provides, with a significantly reduced computational effort, good predictions of critical pressure, of the type of collapse (global or partial) in layered soils, and of its geometry. The mechanism is then employed to conduct parametric studies of the influence of several geometrical and mechanical parameters on face stability of tunnels in layered soils. Similarly, the methodology has been further employed to develop simple design charts that provide the face collapse pressure of tunnels driven by TBM in low quality rock masses and to study the influence of the construction method. Finally, a reliability analysis of the stability of a tunnel face driven in a highly fractured rock mass is performed. The objective is to analyze how different assumptions about distributions types and correlation structures affect the reliability results. In addition, the sensitivity of the reliability index to changes in the random variables is studied, identifying the most relevant variables for engineering design. Finally, an experimental study is carried out using a small-scale laboratory model. The problem is modeled in half, cutting through the tunnel axis vertically, so that displacements of soil particles can be recorded by a digital image correlation technique. The tests were performed with dry sand and displacements are controlled by a piston that supports the soil. The results of the model are compared with the predictions of the Limit Analysis mechanism. A reasonable agreement, according to literature, is obtained between the shapes of the failure surfaces and between the collapse pressures observed in the model tests and computed with the analytical solution.

Shake-table tests of a reinforced concrete frame designed following modern codes: seismic performance and damage evaluation

This paper presents shake-table tests conducted on a two-fifths-scale reinforced concrete frame representing a conventional construction design under current building code provisions in the Mediterranean area. The structure was subjected to a sequence of dynamic tests including free vibrations and four seismic simulations in which a historical ground motion record was scaled to levels of increasing intensity until collapse. Each seismic simulation was associated with a different level of seismic hazard, representing very frequent, frequent, rare and very rare earthquakes. The structure remained basically undamaged and within the inter-story drift limits of the "immediate occupancy" performance level for the very frequent and frequent earthquakes. For the rare earthquake, the specimen sustained significant damage with chord rotations of up to 28% of its ultimate capacity and approached the upper bound limit of inter-story drift associated with "life safety". The specimen collapsed at the beginning of the "very rare" seismic simulation. Besides summarizing the experimental program, this paper evaluates the damage quantitatively at the global and local levels in terms of chord rotation and other damage indexes, together with the energy dissipation demands for each level of seismic hazard. Further, the ratios of column-to-beam moment capacity recommended by Eurocode 8 and ACI-318 to guarantee the formation of a strong column-weak beam mechanism are examined.

Problemas geométricos de localización

En esta memoria estudiamos problemas geométricos relacionados con la Localización de Servicios. La Localización de Servicios trata de la ubicación de uno o más recursos (radares, almacenes, pozos exploradores de petróleo, etc) de manera tal que se optimicen ciertos objetivos (servir al mayor número de usuarios posibles, minimizar el coste de transporte, evitar la contaminación de poblaciones cercanas, etc). La resolución de este tipo de problemas de la vida real da lugar a problemas geométricos muy interesantes. En el planteamiento geométrico de muchos de estos problemas los usuarios potenciales del servicio son representados por puntos mientras que los servicios están representados por la figura geométrica que mejor se adapta al servicio prestado: un anillo para el caso de radares, antenas de radio y televisión, aspersores, etc, una cuña si el servicio que se quiere prestar es de iluminación, por ejemplo, etc. Estas son precisamente las figuras geométricas con las que hemos trabajado. En nuestro caso el servicio será sólo uno y el planteamiento formal del problema es como sigue: dado un anillo o una cuña de tamaño fijo y un conjunto de n puntos en el plano, hallar cuál tiene que ser la posición del mismo para que se cubra la mayor cantidad de puntos. Para resolver estos problemas hemos utilizado arreglos de curvas en el plano. Los arreglos son una estructura geométrica bien conocida y estudiada dentro de la Geometría Computacional. Nosotros nos hemos centrado en los arreglos de curvas de Jordán no acotadas que se intersectan dos a dos en a lo sumo dos puntos, ya que estos fueron los arreglos con los que hemos tenido que tratar para la resolución de los problemas. De entre las diferentes técnicas para la construcción de arreglos hemos estudiado el método incremental, ya que conduce a algoritmos que son en general más sencillos desde el punto de vista de la codificación. Como resultado de este estudio hemos obtenido nuevas cotas que mejoran la complejidad del tiempo de construcción de estos arreglos con algoritmos incrementales. La nueva cota Ο(n λ3(n)) supone una mejora respecto a la cota conocida hasta el momento: Ο(nλ4(n)).También hemos visto que en ciertas condiciones estos arreglos pueden construirse en tiempo Ο(nλ2(n)), que es la cota óptima para la construcción de estos arreglos. Restringiendo el estudio a curvas específicas, hemos obtenido que los arreglos de n circunferencias de k radios diferentes pueden construirse en tiempo Ο(n2 min(log(k),α(n))), resultado válido también para arreglos de elipses, parábolas o hipérbolas de tamaños diferentes cuando las figuras son todas isotéticas.---ABSTRACT--- In this work some geometric problems related with facility location are studied. Facility location deals with location of one or more facilities (radars, stores, oil wells, etc.) in such way that some objective functions are to be optimized (to cover the maximum number of users, to minimize the cost of transportation, to avoid pollution in the nearby cities, etc.). These kind of real world problems give rise to very interesting geometrical problems. In the geometric version of many of these problems, users are represented as points while facilities are represented as different geometric objects depending on the shape of the corresponding facility: an annulus in the case of radars, radio or TV antennas, agricultural spraying devices, etc. A wedge in many illumination or surveillance applications. These two shapes are the geometric figures considered in this Thesis. The formal setting of the problem is the following: Given an annulus or a wedge of fixed size and a set of n points in the plane, locate the best position for the annulus or the wedge so that it covers as many points as possible. Those problems are solved by using arrangements of curves in the plane. Arrangements are a well known geometric structure. Here one deals with arrangements of unbounded Jordan curves which intersect each other in at most two points. Among the different techniques for computing arrangements, incremental method is used because it is easier for implementations. New time complexity upper bounds has been obtained in this Thesis for the construction of such arrangements by means of incremental algorithms. New upper bound is Ο(nλ3(n)) which improves the best known up to now Ο(nλ4(n)). It is shown also that sometimes this arrangements can be constructed in Ο(nλ2(n)), which is the optimal bound for constructing these arrangements. With respect to specific type of curves, one gives an Ο(n2 min(log(k),α(n))), algorithm that constructs the arrangement of a set of n circles of k different radii. This algorithm is also valid for ellipses parabolas or hyperbolas of k different sizes when all of them are isothetic.

On the Insurmountable Size of Truss-like Structures

Galileo postulated the existence of an insurmountable size for stone columns bearing a useful load as the size for which the structure is only able to resist its self-weight. Herein a method for the determination of the unsurmountable size for truss-like structures is shown, given the form of these structures and the ratio between the allowable stress and the specific weight of the material (the material structural scope). Three types of bars are considered: straight bars, with solid and hollow rectangular cross-section, and catenary bars with circular cross-section —a limit and theoretical case for estimating a meaningful upper bound of the structural scope—. An approximate rule to estimate the structural efficiency —here named GA rule— is shown, and is compared with numerical solutions using the proposed method.

Improved static analysis and verification of energy consumption and other resources via abstract interpretation

Resource analysis aims at inferring the cost of executing programs for any possible input, in terms of a given resource, such as the traditional execution steps, time ormemory, and, more recently energy consumption or user defined resources (e.g., number of bits sent over a socket, number of database accesses, number of calls to particular procedures, etc.). This is performed statically, i.e., without actually running the programs. Resource usage information is useful for a variety of optimization and verification applications, as well as for guiding software design. For example, programmers can use such information to choose different algorithmic solutions to a problem; program transformation systems can use cost information to choose between alternative transformations; parallelizing compilers can use cost estimates for granularity control, which tries to balance the overheads of task creation and manipulation against the benefits of parallelization. In this thesis we have significatively improved an existing prototype implementation for resource usage analysis based on abstract interpretation, addressing a number of relevant challenges and overcoming many limitations it presented. The goal of that prototype was to show the viability of casting the resource analysis as an abstract domain, and howit could overcome important limitations of the state-of-the-art resource usage analysis tools. For this purpose, it was implemented as an abstract domain in the abstract interpretation framework of the CiaoPP system, PLAI.We have improved both the design and implementation of the prototype, for eventually allowing an evolution of the tool to the industrial application level. The abstract operations of such tool heavily depend on the setting up and finding closed-form solutions of recurrence relations representing the resource usage behavior of program components and the whole program as well. While there exist many tools, such as Computer Algebra Systems (CAS) and libraries able to find closed-form solutions for some types of recurrences, none of them alone is able to handle all the types of recurrences arising during program analysis. In addition, there are some types of recurrences that cannot be solved by any existing tool. This clearly constitutes a bottleneck for this kind of resource usage analysis. Thus, one of the major challenges we have addressed in this thesis is the design and development of a novel modular framework for solving recurrence relations, able to combine and take advantage of the results of existing solvers. Additionally, we have developed and integrated into our novel solver a technique for finding upper-bound closed-form solutions of a special class of recurrence relations that arise during the analysis of programs with accumulating parameters. Finally, we have integrated the improved resource analysis into the CiaoPP general framework for resource usage verification, and specialized the framework for verifying energy consumption specifications of embedded imperative programs in a real application, showing the usefulness and practicality of the resulting tool.---ABSTRACT---El Análisis de recursos tiene como objetivo inferir el coste de la ejecución de programas para cualquier entrada posible, en términos de algún recurso determinado, como pasos de ejecución, tiempo o memoria, y, más recientemente, el consumo de energía o recursos definidos por el usuario (por ejemplo, número de bits enviados a través de un socket, el número de accesos a una base de datos, cantidad de llamadas a determinados procedimientos, etc.). Ello se realiza estáticamente, es decir, sin necesidad de ejecutar los programas. La información sobre el uso de recursos resulta muy útil para una gran variedad de aplicaciones de optimización y verificación de programas, así como para asistir en el diseño de los mismos. Por ejemplo, los programadores pueden utilizar dicha información para elegir diferentes soluciones algorítmicas a un problema; los sistemas de transformación de programas pueden utilizar la información de coste para elegir entre transformaciones alternativas; los compiladores paralelizantes pueden utilizar las estimaciones de coste para realizar control de granularidad, el cual trata de equilibrar el coste debido a la creación y gestión de tareas, con los beneficios de la paralelización. En esta tesis hemos mejorado de manera significativa la implementación de un prototipo existente para el análisis del uso de recursos basado en interpretación abstracta, abordando diversos desafíos relevantes y superando numerosas limitaciones que éste presentaba. El objetivo de dicho prototipo era mostrar la viabilidad de definir el análisis de recursos como un dominio abstracto, y cómo se podían superar las limitaciones de otras herramientas similares que constituyen el estado del arte. Para ello, se implementó como un dominio abstracto en el marco de interpretación abstracta presente en el sistema CiaoPP, PLAI. Hemos mejorado tanto el diseño como la implementación del mencionado prototipo para posibilitar su evolución hacia una herramienta utilizable en el ámbito industrial. Las operaciones abstractas de dicha herramienta dependen en gran medida de la generación, y posterior búsqueda de soluciones en forma cerrada, de relaciones recurrentes, las cuales modelizan el comportamiento, respecto al consumo de recursos, de los componentes del programa y del programa completo. Si bien existen actualmente muchas herramientas capaces de encontrar soluciones en forma cerrada para ciertos tipos de recurrencias, tales como Sistemas de Computación Algebraicos (CAS) y librerías de programación, ninguna de dichas herramientas es capaz de tratar, por sí sola, todos los tipos de recurrencias que surgen durante el análisis de recursos. Existen incluso recurrencias que no las puede resolver ninguna herramienta actual. Esto constituye claramente un cuello de botella para este tipo de análisis del uso de recursos. Por lo tanto, uno de los principales desafíos que hemos abordado en esta tesis es el diseño y desarrollo de un novedoso marco modular para la resolución de relaciones recurrentes, combinando y aprovechando los resultados de resolutores existentes. Además de ello, hemos desarrollado e integrado en nuestro nuevo resolutor una técnica para la obtención de cotas superiores en forma cerrada de una clase característica de relaciones recurrentes que surgen durante el análisis de programas lógicos con parámetros de acumulación. Finalmente, hemos integrado el nuevo análisis de recursos con el marco general para verificación de recursos de CiaoPP, y hemos instanciado dicho marco para la verificación de especificaciones sobre el consumo de energía de programas imperativas embarcados, mostrando la viabilidad y utilidad de la herramienta resultante en una aplicación real.