Abstract interpretation with specialized definitions

The relationship between abstract interpretation and partial evaluation has received considerable attention and (partial) integrations have been proposed starting from both the partial evaluation and abstract interpretation perspectives. In this work we present what we argüe is the first generic algorithm for efñcient and precise integration of abstract interpretation and partial evaluation from an abstract interpretation perspective. Taking as starting point state-of-the-art algorithms for context-sensitive, polyvariant abstract interpretation and (abstract) partial evaluation of logic programs, we present an algorithm which combines the best of both worlds. Key ingredients include the accurate success propagation inherent to abstract interpretation and the powerful program transformations achievable by partial deduction. In our algorithm, the calis which appear in the analysis graph are not analyzed w.r.t. the original definition of the procedure but w.r.t. specialized definitions of these procedures. Such specialized definitions are obtained by applying both unfolding and abstract executability. Also, our framework is parametric w.r.t. different control strategies and abstract domains. Different combinations of these parameters correspond to existing algorithms for program analysis and specialization. Our approach efficiently computes strictly more precise results than those achievable by each of the individual techniques. The algorithm is one of the key components of CiaoPP, the analysis and specialization system of the Ciao compiler.

What Makes an Effective Abstract in Sport Science?

Writing an efficient abstract is always a difficult and significant work in academic writing. What kinds of abstracts are well reputed in sport science? To answer this question, 20 abstracts from top journals of sport science were analyzed in the current research. The number of words and rhetorical moves were studied to assess the structures of the abstracts. Meanwhile, the key clauses, citations, the use of first person pronoun, the adoption of abbreviations and acronyms, hedging and the main tense were included in the analysis of the writing skills. Results have show: (1) Almost all of the abstracts were non-structured, and the length varied a lot, but the average word count was about 210-220; (2) the use of writing skills, such as key clauses, citations and hedging differed depending on the preference of the journal where the abstract appeared, and the main tense was selected based on the context of the abstract. In most cases, abbreviations and acronyms were allowed to be used, while the first person pronoun was always avoided

Towards an abstract domain for resource analysis of logic programs using sized types

We present a novel general resource analysis for logic programs based on sized types.Sized types are representations that incorporate structural (shape) information and allow expressing both lower and upper bounds on the size of a set of terms and their subterms at any position and depth. They also allow relating the sizes of terms and subterms occurring at different argument positions in logic predicates. Using these sized types, the resource analysis can infer both lower and upper bounds on the resources used by all the procedures in a program as functions on input term (and subterm) sizes, overcoming limitations of existing analyses and enhancing their precision. Our new resource analysis has been developed within the abstract interpretation framework, as an extension of the sized types abstract domain, and has been integrated into the Ciao preprocessor, CiaoPP. The abstract domain operations are integrated with the setting up and solving of recurrence equations for both, inferring size and resource usage functions. We show that the analysis is an improvement over the previous resource analysis present in CiaoPP and compares well in power to state of the art systems.

Resource usage analysis of logic programs via abstract interpretation using sized types

We present a novel general resource analysis for logic programs based on sized types. Sized types are representations that incorporate structural (shape) information and allow expressing both lower and upper bounds on the size of a set of terms and their subterms at any position and depth. They also allow relating the sizes of terms and subterms occurring at different argument positions in logic predicates. Using these sized types, the resource analysis can infer both lower and upper bounds on the resources used by all the procedures in a program as functions on input term (and subterm) sizes, overcoming limitations of existing resource analyses and enhancing their precision. Our new resource analysis has been developed within the abstract interpretation framework, as an extension of the sized types abstract domain, and has been integrated into the Ciao preprocessor, CiaoPP. The abstract domain operations are integrated with the setting up and solving of recurrence equations for inferring both size and resource usage functions. We show that the analysis is an improvement over the previous resource analysis present in CiaoPP and compares well in power to state of the art systems.

La identificaciónde de los daños estructurales, herramienta de la nueva atribución de responsabilidades : análisis crítico de la transición del art. 1591 cc al art. 17 LOE

RESUMEN Su objetivo esencial: Regular el proceso de la edificación, está basado en 3 grandes pilares: 1.- Completar la configuración legal de los agentes que intervienen en el mismo, fijando sus obligaciones para así establecer las responsabilidades. 2.- Fomentar la calidad de los edificios. 3.- Fijar las garantías a los usuarios frente a los posibles daños. Estos tres fundamentos están intensamente relacionados, ya que, las obligaciones y responsabilidades de los agentes son la base de la constitución de las garantías a los usuarios, definidas mediante los requisitos básicos que deben satisfacer los edificios. Partiendo del análisis cualitativo y cuantitativo del grado de cumplimiento del objetivo de la nueva Ley, elaborado a través del estudio de sus tres pilares fundamentales, proponemos medidas tendentes a la plena entrada en vigor de la misma. Para ello se deberá desarrollar el Real Decreto previsto en la Disposición Adicional 2ª, una vez conseguido el grado de madurez de los sectores de la edificación y del seguro. En todo este proceso de estudio hemos podido apreciar que la objetiva identificación de los daños y en especial los que afectan la estabilidad del edificio, constituye una herramienta fundamental para la correcta atribución de responsabilidades a los agentes, basada en la aplicación de los tres grados de responsabilidad “ex lege” por daños materiales y sus plazos de prescripción surgidos del nuevo régimen impuesto por el art. 17 LOE Para avalar esta propuesta hemos analizado: 1.- El entorno económico, general y pormenorizado al sector de la edificación, en Europa y España durante el período comprendido entre los años 1990 y 2013, años previos y posteriores a la entrada en vigor de la Ley, dada la influencia de los ciclos de actividad producidos en la regulación del sector, las responsabilidades atribuidas a los agentes, el fomento de la calidad y las garantías ofrecidas a los adquirentes. 2.- Las diversas legislaciones sobre responsabilidades y garantías de los agentes de la edificación en los países de nuestro entorno económico. 3.- La gestación de la LOE, incidiendo en la evolución de los últimos borradores y su tramitación parlamentaria. 4.- El desarrollo doctrinal de la Transición desde el régimen de responsabilidades, fijado por el art. 1591 de Código Civil, y su Jurisprudencia, hacia el nuevo régimen de responsabilidades establecido por el art. 17 LOE. En esta tarea además de apreciar la asimilación, por parte de los Jueces y Magistrados, de los principios doctrinales de la LOE, hemos observado la labor de los peritos, de cuya experta identificación de las causas de los daños depende la justa y eficaz atribución de responsabilidades. 5 -. El grado de eficacia de la LOE a la vista de la estadística siniestral, de la que ya hay datos consolidados, tras la cancelación de casi 15.000 expedientes de reclamación a Arquitectos. 6 -. También hemos estudiado el grado de cumplimiento con el usuario y propietario de las garantías previstas en el art. 19 de la Ley y en la D.A. 1ª, los efectos reales alcanzados y las tareas pendientes por delante. Analizando la atribución de responsabilidades a los agentes de la edificación, dentro del primer pilar fundamental de la LOE, hemos estudiado las actuaciones de los peritos expertos y su incidencia en este objetivo, previa selección de casos de gran interés y dificultad. Fruto de ello se han formulado propuestas tendentes a la especialización de este colectivo, evitando conductas “irregulares” que tanto daño provocan a los agentes reclamados como a los propietarios afectados. Este daño es evidente pudiendo ocasionar condenas injustas, enriquecimientos ilícitos o bien falsas expectativas de satisfacción de daños mal dictaminados y costosas e ineficaces reparaciones. De cara a la consecución del pilar de la calidad de la edificación, mediante los requisitos básicos planteados por la LOE y desarrollados por el Código Técnico de la Edificación (Real Decreto 314/2006, de 17 de marzo), hemos procesado datos de expedientes de reclamaciones por daños que afectan a edificios ejecutados bajo el nuevo régimen LOE. Con esta base se han analizado las causas generadoras de las diversas lesiones y su frecuencia para que de este análisis puedan establecerse pautas de actuación para su prevención. Finalmente, tras demostrar que las garantías obligatorias impuestas por la LOE sólo abarcan un pequeño porcentaje de los posibles daños a la edificación, insistimos en la necesidad de la plena eficacia de la Ley mediante la aprobación de todas las garantías previstas y para todo tipo de edificaciones. En suma, se ha diseñado la tesis como una matriz abierta en la que podremos continuar incorporando datos de la evolución de la doctrina, la jurisprudencia y la estadística de los daños en la edificación. ABSTRACT The approval of Law 38/1999 on November 5, 1999, (Official Gazette BOE 266/1999 of 11.6.1999, p. 38925), was the culmination of a long period of over 20 years of gestation for which deep agreements were needed between all stakeholders affected. Although several parliamentary groups denounced its incomplete approval, regarding mandatory guarantees to the purchaser, its enactment caused general satisfaction among most of the the building agents. This assessment remains after fourteen years since its partial enactment. Its essential purpose, “to regulate the building process”, is based on 3 pillars: 1.- To complete the legal configuration of the agents involved in it, setting their obligations in order to establish their responsibilities. 2.- To promote the buildings quality. 3.- To specify users´guarantees against possible buildings damage. These three issues are strongly related, since the obligations and responsibilities of the actors are the basis of the users’guarantees constitution, defined by the basic performance required by buildings. Based on the qualitative and quantitative analysis of the fulfillment of the new law’s objectives, made by monitoring the three pillars, we propose measures to the full enactment of this Directive, by the development of the Royal Decree, provided in its Second Additional Provision, once maturity in the sectors of the building and insurance is achieved. Throughout this process of study we have seen that the skill identification of damage, particularly those affecting the stability of the building, is an essential tool for the proper allocation of responsibilities of the new regime installed by the art. 17 LOE, based on the application of the three degrees of responsibility "ex lege" for property damage and limitation periods. To support this proposal, we have analyzed: 1.- The evolution of the building sector in Europe and Spain during the years before and after the enactment of the Law, due to the influence of cycles of activity produced in industry regulation, the responsibilities attributed to agents, promotion of the quality and the assurances given to acquirers. 2.- The scope of various laws on liability and building agents warranties in the countries of our economic environment. 3.- The long period of LOE generation, focusing on the developments in recent drafts and parliamentary procedure. 4.- The doctrinal development in the Transition from the regime of responsibilities, set by art. 1591 of the Civil Code, and its Jurisprudence, to the new liability regime established by art. 17 LOE. In this task, while we have noted assimilation by the Judges and Magistrates of the doctrinal principles of the LOE, we have also analyzed the work of experts, whose skilled identification of the damage causes helps the fair and efficient allocation of responsibilities. 5 - The effectiveness of the LOE based on knowledge of the siniestral statistics, which are already consolidated data, after the cancellation of nearly 15,000 claims to Architects. 6.- We have also studied the degree of compliance with the user and owner guarantees, established in art. 19 and the D.A. 1th of the LOE, exposing the real effects achieved and the pending tasks ahead. Analyzing the allocation of the building agents´ responsibilities, within the first cornerstone of the LOE, we have studied the expert witnesses actions and their impact on this duty, selecting cases of great interest and difficulty in this aim. The result of this enterprise has been to propose the specialization of this group, avoiding "irregular" behaviors that create as much damage as the agents claimed to affected owners. This damage is evident and can cause wrong convictions, illicit enrichment, false expectations and inefficient and costly damage repairs. In order to achieve the pillar of building quality through the basic requirements set by the LOE and developed by the Technical Building Code (Royal Decree 314/ 2006 of 17 March), we have analyzed records of damage claims involving buildings executed under the new regime LOE. On this basis we have analyzed the root causes of various damages and their frequency, from these data it will be easy to propose lines of action for prevention. Finally, after demonstrating that mandatory warranties imposed by LOE cover only a small percentage of the potential building damage, we emphasize the need for the full effectiveness of the Law by the obligation all the guarantees provided in the art. 19 LOE, and for all types of buildings. In conclusion, this thesis is designed as an open matrix in which we will continue including data on the evolution of the doctrine, jurisprudence and the statistics of the damage to the building.

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.