Generation of reduced certificates in abstraction-carrying code

Abstraction-Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certifícate and its generation is carried out automatically by a fixed-point analyzer. The advantage of providing a (fixedpoint) abstraction to the code consumer is that its validity is checked in a single pass of an abstract interpretation-based checker. A main challenge is to reduce the size of certificates as much as possible while at the same time not increasing checking time. In this paper, we first introduce the notion of reduced certifícate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certifícate in a single pass. Based on this notion, we then instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker.

Reduced certificates for abstraction-carrying code

Abstraction-Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certifícate and its generation is carried out automatically by a fixed-point analyzer. The advantage of providing a (fixed-point) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible while at the same time not increasing checking time. The intuitive idea is to only include in the certifícate information that the checker is unable to reproduce without iterating. We introduce the notion of reduced certifícate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certifícate in a single pass. Based on this notion, we instrument a generic analysis algorithm with the necessary extensions in order to identify information which can be reconstructed by the single-pass checker. Finally, we study what the effects of reduced certificates are on the correctness and completeness of the checking process. We provide a correct checking algorithm together with sufficient conditions for ensuring its completeness. Our ideas are illustrated through a running example, implemented in the context of constraint logic programs, which shows that our approach improves state-of-the-art techniques for reducing the size of certificates.

Advanced Topics in Resource Analysis: Certification, Incrementality, Concurrency and Array-Sensitivity

El Análisis de Consumo de Recursos o Análisis de Coste trata de aproximar el coste de ejecutar un programa como una función dependiente de sus datos de entrada. A pesar de que existen trabajos previos a esta tesis doctoral que desarrollan potentes marcos para el análisis de coste de programas orientados a objetos, algunos aspectos avanzados, como la eficiencia, la precisión y la fiabilidad de los resultados, todavía deben ser estudiados en profundidad. Esta tesis aborda estos aspectos desde cuatro perspectivas diferentes: (1) Las estructuras de datos compartidas en la memoria del programa son una pesadilla para el análisis estático de programas. Trabajos recientes proponen una serie de condiciones de localidad para poder mantener de forma consistente información sobre los atributos de los objetos almacenados en memoria compartida, reemplazando éstos por variables locales no almacenadas en la memoria compartida. En esta tesis presentamos dos extensiones a estos trabajos: la primera es considerar, no sólo los accesos a los atributos, sino también los accesos a los elementos almacenados en arrays; la segunda se centra en los casos en los que las condiciones de localidad no se cumplen de forma incondicional, para lo cual, proponemos una técnica para encontrar las precondiciones necesarias para garantizar la consistencia de la información acerca de los datos almacenados en memoria. (2) El objetivo del análisis incremental es, dado un programa, los resultados de su análisis y una serie de cambios sobre el programa, obtener los nuevos resultados del análisis de la forma más eficiente posible, evitando reanalizar aquellos fragmentos de código que no se hayan visto afectados por los cambios. Los analizadores actuales todavía leen y analizan el programa completo de forma no incremental. Esta tesis presenta un análisis de coste incremental, que, dado un cambio en el programa, reconstruye la información sobre el coste del programa de todos los métodos afectados por el cambio de forma incremental. Para esto, proponemos (i) un algoritmo multi-dominio y de punto fijo que puede ser utilizado en todos los análisis globales necesarios para inferir el coste, y (ii) una novedosa forma de almacenar las expresiones de coste que nos permite reconstruir de forma incremental únicamente las funciones de coste de aquellos componentes afectados por el cambio. (3) Las garantías de coste obtenidas de forma automática por herramientas de análisis estático no son consideradas totalmente fiables salvo que la implementación de la herramienta o los resultados obtenidos sean verificados formalmente. Llevar a cabo el análisis de estas herramientas es una tarea titánica, ya que se trata de herramientas de gran tamaño y complejidad. En esta tesis nos centramos en el desarrollo de un marco formal para la verificación de las garantías de coste obtenidas por los analizadores en lugar de analizar las herramientas. Hemos implementado esta idea mediante la herramienta COSTA, un analizador de coste para programas Java y KeY, una herramienta de verificación de programas Java. De esta forma, COSTA genera las garantías de coste, mientras que KeY prueba la validez formal de los resultados obtenidos, generando de esta forma garantías de coste verificadas. (4) Hoy en día la concurrencia y los programas distribuidos son clave en el desarrollo de software. Los objetos concurrentes son un modelo de concurrencia asentado para el desarrollo de sistemas concurrentes. En este modelo, los objetos son las unidades de concurrencia y se comunican entre ellos mediante llamadas asíncronas a sus métodos. La distribución de las tareas sugiere que el análisis de coste debe inferir el coste de los diferentes componentes distribuidos por separado. En esta tesis proponemos un análisis de coste sensible a objetos que, utilizando los resultados obtenidos mediante un análisis de apunta-a, mantiene el coste de los diferentes componentes de forma independiente. Abstract Resource Analysis (a.k.a. Cost Analysis) tries to approximate the cost of executing programs as functions on their input data sizes and without actually having to execute the programs. While a powerful resource analysis framework on object-oriented programs existed before this thesis, advanced aspects to improve the efficiency, the accuracy and the reliability of the results of the analysis still need to be further investigated. This thesis tackles this need from the following four different perspectives. (1) Shared mutable data structures are the bane of formal reasoning and static analysis. Analyses which keep track of heap-allocated data are referred to as heap-sensitive. Recent work proposes locality conditions for soundly tracking field accesses by means of ghost non-heap allocated variables. In this thesis we present two extensions to this approach: the first extension is to consider arrays accesses (in addition to object fields), while the second extension focuses on handling cases for which the locality conditions cannot be proven unconditionally by finding aliasing preconditions under which tracking such heap locations is feasible. (2) The aim of incremental analysis is, given a program, its analysis results and a series of changes to the program, to obtain the new analysis results as efficiently as possible and, ideally, without having to (re-)analyze fragments of code that are not affected by the changes. During software development, programs are permanently modified but most analyzers still read and analyze the entire program at once in a non-incremental way. This thesis presents an incremental resource usage analysis which, after a change in the program is made, is able to reconstruct the upper-bounds of all affected methods in an incremental way. To this purpose, we propose (i) a multi-domain incremental fixed-point algorithm which can be used by all global analyses required to infer the cost, and (ii) a novel form of cost summaries that allows us to incrementally reconstruct only those components of cost functions affected by the change. (3) Resource guarantees that are automatically inferred by static analysis tools are generally not considered completely trustworthy, unless the tool implementation or the results are formally verified. Performing full-blown verification of such tools is a daunting task, since they are large and complex. In this thesis we focus on the development of a formal framework for the verification of the resource guarantees obtained by the analyzers, instead of verifying the tools. We have implemented this idea using COSTA, a state-of-the-art cost analyzer for Java programs and KeY, a state-of-the-art verification tool for Java source code. COSTA is able to derive upper-bounds of Java programs while KeY proves the validity of these bounds and provides a certificate. The main contribution of our work is to show that the proposed tools cooperation can be used for automatically producing verified resource guarantees. (4) Distribution and concurrency are today mainstream. Concurrent objects form a well established model for distributed concurrent systems. In this model, objects are the concurrency units that communicate via asynchronous method calls. Distribution suggests that analysis must infer the cost of the diverse distributed components separately. In this thesis we propose a novel object-sensitive cost analysis which, by using the results gathered by a points-to analysis, can keep the cost of the diverse distributed components separate.

A non-perturbative renormalization group study of the stochastic NavierStokes equation

We study the renormalization group flow of the average action of the stochastic Navier-Stokes equation with power-law forcing. Using Galilean invariance, we introduce a nonperturbative approximation adapted to the zero-frequency sector of the theory in the parametric range of the Hölder exponent 4−2 ɛ of the forcing where real-space local interactions are relevant. In any spatial dimension d, we observe the convergence of the resulting renormalization group flow to a unique fixed point which yields a kinetic energy spectrum scaling in agreement with canonical dimension analysis. Kolmogorov's −5/3 law is, thus, recovered for ɛ=2 as also predicted by perturbative renormalization. At variance with the perturbative prediction, the −5/3 law emerges in the presence of a saturation in the ɛ dependence of the scaling dimension of the eddy diffusivity at ɛ=3/2 when, according to perturbative renormalization, the velocity field becomes infrared relevant.

Floating car data augmentation based on infrastructure sensors and neural networks

The development of new-generation intelligent vehicle technologies will lead to a better level of road safety and CO2 emission reductions. However, the weak point of all these systems is their need for comprehensive and reliable data. For traffic data acquisition, two sources are currently available: 1) infrastructure sensors and 2) floating vehicles. The former consists of a set of fixed point detectors installed in the roads, and the latter consists of the use of mobile probe vehicles as mobile sensors. However, both systems still have some deficiencies. The infrastructure sensors retrieve information fromstatic points of the road, which are spaced, in some cases, kilometers apart. This means that the picture of the actual traffic situation is not a real one. This deficiency is corrected by floating cars, which retrieve dynamic information on the traffic situation. Unfortunately, the number of floating data vehicles currently available is too small and insufficient to give a complete picture of the road traffic. In this paper, we present a floating car data (FCD) augmentation system that combines information fromfloating data vehicles and infrastructure sensors, and that, by using neural networks, is capable of incrementing the amount of FCD with virtual information. This system has been implemented and tested on actual roads, and the results show little difference between the data supplied by the floating vehicles and the virtual vehicles.

Analytical properties of horizontal visibility graphs in the Feigenbaum scenario

Time series are proficiently converted into graphs via the horizontal visibility (HV) algorithm, which prompts interest in its capability for capturing the nature of different classes of series in a network context. We have recently shown [B. Luque et al., PLoS ONE 6, 9 (2011)] that dynamical systems can be studied from a novel perspective via the use of this method. Specifically, the period-doubling and band-splitting attractor cascades that characterize unimodal maps transform into families of graphs that turn out to be independent of map nonlinearity or other particulars. Here, we provide an in depth description of the HV treatment of the Feigenbaum scenario, together with analytical derivations that relate to the degree distributions, mean distances, clustering coefficients, etc., associated to the bifurcation cascades and their accumulation points. We describe how the resultant families of graphs can be framed into a renormalization group scheme in which fixed-point graphs reveal their scaling properties. These fixed points are then re-derived from an entropy optimization process defined for the graph sets, confirming a suggested connection between renormalization group and entropy optimization. Finally, we provide analytical and numerical results for the graph entropy and show that it emulates the Lyapunov exponent of the map independently of its sign.

A generic, hard transition to chaos

A hard-in-amplitude transition to chaos in a class of dissipative flows of broad applicability is presented. For positive values of a parameter F, no matter how small, a fully developed chaotic attractor exists within some domain of additional parameters, whereas no chaotic behavior exists for F < 0. As F is made positive, an unstable fixed point reaches an invariant plane to enter a phase half-space of physical solutions; the ghosts of a line of fixed points and a rich heteroclinic structure existing at F = 0 make the limits t --* +oc, F ~ +0 non-commuting, and allow an exact description of the chaotic flow. The formal structure of flows that exhibit the transition is determined. A subclass of such flows (coupled oscillators in near-resonance at any 2 : q frequency ratio, with F representing linear excitation of the first oscillator) is fully analysed

Damping models in the truncated derivative nonlinear Schrödinger equation

Four-dimensional flow in the phase space of three amplitudes of circularly polarized Alfven waves and one relative phase, resulting from a resonant three-wave truncation of the derivative nonlinear Schrödinger equation, has been analyzed; wave 1 is linearly unstable with growth rate , and waves 2 and 3 are stable with damping 2 and 3, respectively. The dependence of gross dynamical features on the damping model as characterized by the relation between damping and wave-vector ratios, 2 /3, k2 /k3, and the polarization of the waves, is discussed; two damping models, Landau k and resistive k2, are studied in depth. Very complex dynamics, such as multiple blue sky catastrophes and chaotic attractors arising from Feigenbaum sequences, and explosive bifurcations involving Intermittency-I chaos, are shown to be associated with the existence and loss of stability of certain fixed point P of the flow. Independently of the damping model, P may only exist as against flow contraction just requiring.In the case of right-hand RH polarization, point P may exist for all models other than Landau damping; for the resistive model, P may exist for RH polarization only if 2+3/2.

Non-periodic driving of coupled oscillators:a spherical swing

Nonlinearly coupled, damped oscillators at 1:1 frequency ratio, one oscillator being driven coherently for efficient excitation, are exemplified by a spherical swing with some phase-mismatch between drive and response. For certain damping range, excitation is found to succeed if it lags behind, but to produce a chaotic attractor if it leads the response. Although a period-doubhng sequence, for damping increasing, leads to the attractor, this is actually born as a hard (as regards amplitude) bifurcation at a zero growth-rate parametric line; as damping decreases, an unstable fixed point crosses an invariant plane to enter as saddle-focus a phase-space domain of physical solutions. A second hard bifurcation occurs at the zero mismatch line, the saddle-focus leaving that domain. Times on the attractor diverge when approaching either fine, leading to exactly one-dimensional and noninvertible limit maps, which are analytically determined.

Sudden transition to chaos in plasma wave interactions

The coherent three-wave interaction, with linear growth in the higher frequency wave and damping in the two other waves, is reconsidered; for equal dampings, the resulting three-dimensional (3-D) flow of a relative phase and just two amplitudes behaved chaotically, no matter how small the growth of the unstable wave. The general case of different dampings is studied here to test whether, and how, that hard scenario for chaos is preserved in passing from 3-D to four-dimensional flows. It is found that the wave with higher damping is partially slaved to the other damped wave; this retains a feature of the original problem an invariant surface that meets an unstable fixed point, at zero growth rate! that gave rise to the chaotic attractor and determined its structure, and suggests that the sudden transition to chaos should appear in more complex wave interactions.

A method for revealing phase space structures of general time dependent dynamical systems

In this paper we develop new techniques for revealing geometrical structures in phase space that are valid for aperiodically time dependent dynamical systems, which we refer to as Lagrangian descriptors. These quantities are based on the integration, for a finite time, along trajectories of an intrinsic bounded, positive geometrical and/or physical property of the trajectory itself. We discuss a general methodology for constructing Lagrangian descriptors, and we discuss a “heuristic argument” that explains why this method is successful for revealing geometrical structures in the phase space of a dynamical system. We support this argument by explicit calculations on a benchmark problem having a hyperbolic fixed point with stable and unstable manifolds that are known analytically. Several other benchmark examples are considered that allow us the assess the performance of Lagrangian descriptors in revealing invariant tori and regions of shear. Throughout the paper “side-by-side” comparisons of the performance of Lagrangian descriptors with both finite time Lyapunov exponents (FTLEs) and finite time averages of certain components of the vector field (“time averages”) are carried out and discussed. In all cases Lagrangian descriptors are shown to be both more accurate and computationally efficient than these methods. We also perform computations for an explicitly three dimensional, aperiodically time-dependent vector field and an aperiodically time dependent vector field defined as a data set. Comparisons with FTLEs and time averages for these examples are also carried out, with similar conclusions as for the benchmark examples.

Horizontal visibility graphs generated by type-I intermittency

The type-I intermittency route to (or out of) chaos is investigated within the horizontal visibility (HV) graph theory. For that purpose, we address the trajectories generated by unimodal maps close to an inverse tangent bifurcation and construct their associatedHVgraphs.We showhowthe alternation of laminar episodes and chaotic bursts imprints a fingerprint in the resulting graph structure. Accordingly, we derive a phenomenological theory that predicts quantitative values for several network parameters. In particular, we predict that the characteristic power-law scaling of the mean length of laminar trend sizes is fully inherited by the variance of the graph degree distribution, in good agreement with the numerics. We also report numerical evidence on how the characteristic power-law scaling of the Lyapunov exponent as a function of the distance to the tangent bifurcation is inherited in the graph by an analogous scaling of block entropy functionals defined on the graph. Furthermore, we are able to recast the full set of HV graphs generated by intermittent dynamics into a renormalization-group framework, where the fixed points of its graph-theoretical renormalization-group flow account for the different types of dynamics.We also establish that the nontrivial fixed point of this flow coincides with the tangency condition and that the corresponding invariant graph exhibits extremal entropic properties.

Modelización de reacciones químicas en presencia de un campo electromagnético variable

En esta tesis se aborda el estudio del proceso de isomerización del sistema molecular LiNC/LiCN tanto aislado como en presencia de un pulso láser aplicando la teoría del estado de transición (TST). Esta teoría tiene como pilar fundamental el hecho de que el conocimiento de la dinámica en las proximidades de un punto de silla de la superficie de energía potencial permite determinar los parámetros cinéticos de la reacción objeto de estudio. Históricamente, existen dos formulaciones de la teoría del estado de transición, la versión termodinámica de Eyring (Eyr38) y la visión dinámica de Wigner (Wig38). Ésta última ha sufrido recientemente un amplio desarrollo, paralelo a los avances en sistemas dinámicos que ha dado lugar a una formulación geométrica en el espacio de fases que sirve como base al trabajo desarrollado en esta tesis. Nos hemos centrado en abordar el problema desde una visión fundamentalmente práctica, ya que la teoría del estado de transición presenta una desventaja: su elevado coste computacional y de tiempo de cálculo. Dos han sido los principales objetivos de este trabajo. El primero de ellos ha sido sentar las bases teóricas y computacionales de un algoritmo eficiente que permita obtener las magnitudes fundamentales de la TST. Así, hemos adaptado con éxito un algoritmo computacional desarrollado en el ámbito de la mecánica celeste (Jor99), obteniendo un método rápido y eficiente para la obtención de los objetos geométricos que rigen la dinámica en el espacio de fases y que ha permitido calcular magnitudes cinéticas tales como el flujo reactivo, la densidad de estados de reactivos y productos y en última instancia la constante de velocidad. Dichos cálculos han sido comparados con resultados estadísticos (presentados en (Mül07)) lo cual nos ha permitido demostrar la eficacia del método empleado. El segundo objetivo de esta tesis, ha sido la evaluación de la influencia de los parámetros de un pulso electromagnético sobre la dinámica de reacción. Para ello se ha generalizado la metodología de obtención de la forma normal del hamiltoniano cuando el sistema químico es alterado mediante una perturbación temporal periódica. En este caso el punto fijo inestable en cuya vecindad se calculan los objetos geométricos de interés para la aplicación de la TST, se transforma en una órbita periódica del mismo periodo que la perturbación. Esto ha permitido la simulación de la reactividad en presencia de un pulso láser. Conocer el efecto de esta perturbación posibilita el control de la reactividad química. Además de obtener los objetos geométricos que rigen la dinámica en una cierta vecindad de la órbita periódica y que son la clave de la TST, se ha estudiado el efecto de los parámetros del pulso sobre la reactividad en el espacio de fases global así como sobre el flujo reactivo que atraviesa la superficie divisoria que separa reactivos de productos. Así, se ha puesto de manifiesto, que la amplitud del pulso es el parámetro más influyente sobre la reactividad química, pudiendo producir la aparición de flujos reactivos a energías inferiores a las de aparición del sistema aislado y el aumento del flujo reactivo a valores constantes de energía inicial. ABSTRACT We have studied the isomerization reaction LiNC/LiCN isolated and perturbed by a laser pulse. Transition State theory (TST) is the main tool we have used. The basis of this theory is knowing the dynamics close to a fixed point of the potential energy surface. It is possible to calculate kinetic magnitudes by knowing the dynamics in a neighbourhood of the fixed point. TST was first formulated in the 30's and there were 2 points of view, one thermodynamical by Eyring (Eyr38) and another dynamical one by Wigner (Wig38). The latter one has grown lately due to the growth of the dynamical systems leading to a geometrical view of the TST. This is the basis of the work shown in this thesis. As the TST has one main handicap: the high computational cost, one of the main goals of this work is to find an efficient method. We have adapted a methodology developed in the field of celestial mechanics (Jor99). The result: an efficient, fast and accurate algorithm that allows us to obtain the geometric objects that lead the dynamics close to the fixed point. Flux across the dividing surface, density of states and reaction rate coefficient have been calculated and compared with previous statistical results, (Mül07), leading to the conclusion that the method is accurate and good enough. We have widen the methodology to include a time dependent perturbation. If the perturbation is periodic in time, the fixed point becomes a periodic orbit whose period is the same as the period of the perturbation. This way we have been able to simulate the isomerization reaction when the system has been perturbed by a laser pulse. By knowing the effect of that perturbation we will be able to control the chemical reactivity. We have also studied the effect of the parameters on the global phase space dynamics and on the flux across the dividing surface. It has been prove that amplitude is the most influent parameter on the reaction dynamics. Increasing amplitude leads to greater fluxes and to some flux at energies it would not if the systems would not have been perturbed.

Quasiperiodic Graphs: Structural Design, Scaling and Entropic Properties

A novel class of graphs, here named quasiperiodic, are const ructed via application of the Horizontal Visibility algorithm to the time series generated along the quasiperiodic route to chaos. We show how the hierarchy of mode-locked regions represented by the Far ey tree is inherited by their associated graphs. We are able to establish, via Renormalization Group (RG) theory, the architecture of the quasiperiodic graphs produced by irrational winding numbers with pure periodic continued fraction. And finally, we demonstrate that the RG fixed-point degree distributions are recovered via optimization of a suitably defined graph entropy

Ice volume estimates from ground-penetrating radar surveys, Wedel Jarlsberg Land glaciers, Svalbard

One of the aims of the SvalGlac project is to obtain an improved estimate, with reliable error estimates, of the volume of Svalbard glaciers and their potential contribution to sea level rise. As part of this work, we present volume calculations, with detailed error estimates, for eight glaciers on Wedel Jarlsberg Land, southern Spitsbergen, Svalbard. The volume estimates are based upon a dense net of GPR-retrieved ice thickness data collected over several field campaigns spanning the period 2004-2011. The total area and volume of the ensemble are 502.9±18.6 km2 and 80.72±2.85 km3, respectively. Excluding Ariebreen (a tiny glacier, menor que 0.4 km2 in area), the individual areas, volumes and average ice thickness lie within 4.7-141.0 km2, 0.30-25.85 km3 and 64-183 m, respectively. The maximum recorded ice thickness, ca. 619±13 m, is found in Austre Torellbreen. To estimate the ice volume of small non-echo-sounded tributary glaciers, we used a function providing the best fit to the ice thickness along the centre line of a collection of such tributaries where echo-soundings were available, and assuming parabolic cross-sections. We did some tests on the effect on the measured ice volumes of the distinct radio-wave velocity (RWV) of firn as compared to ice, and cold versus temperate ice, concluding that the changes in volume implied by such corrections were within the error bounds of our volume estimate using a constant RWV for the entire glacier inferred from common mid-point measurements on the upper ablation area.