Biblioteca Digital | FCEN-UBA

Biblioteca Digital ¿Por qué?
Objetivos
Impactos
Estadísticas
Documentos
Presentaciones
Notas
Autores y derechos
¿Por qué depositar?
¿Cómo depositar?
Autorización
Depositar y publicar
Editoriales
Publicar mi tesis Formulario Tesis Posgrado
Formulario Tesis Grado
Normativa
Res. CD 2053/05
Res. CD 2533/09
Res. CD 0272/13
Res. CD 2793/15

Colecciones Tesis Doctorales
Fotografías
Publicaciones
Archivo
Libros
Reportes Técnicos

Tesis > TEMA

Computación [ 80 tesis ]

Lógica y Computabilidad [ 4 tesis ]

Arbiser, Ariel. "Sistemas y subsistemas de sustituciones explícitas" (2005) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
Esta tesis trata acerca de alguinos problemas en la teoría de reescritura y cálculos con sustituciónes explícitas. El tema principal es el estudio de sub cálculos de algunos sistemas de reescritura. Luego de una introducción sesgada a la reescritura, el cálculo lamba y las sustituciónes explícitas, hacemos un estudio comparativo de los principales formalismos de la reescritura, identificando una jerarquía entre éstos. Como primer aproximación a nuevos cálculos, estudiamos el cálculo lambda con nombres de Revesz, que utiliza cuatro reglas de reescriotura, con la particularidad de que no cuenta con sustirución alguna. Se prueba la correctitud relativa y la confluencia. También se proponen y se estudian dos versiones que usan índices de de Bruijn, y se prueba que estas dos propiedades se preservan. Luego pasamos a la perpetualidad en el cálculo de sustituciónes explícitas lambda v y estudiamos estrategias de reducción perpertias, i.e. aquellas que preservan la posibilidad de derivaciónes infinitas. Se da como una aplicación un conjunto de reglas de inferencia determinísticas que caracterizan inductivamente el sub sistema de los términos fuertemente normalizantes, y presentamos una estrategia de reducción perpetia efectiva para lambda v. A continuación se estudian distintas extensiones del cálculo lambda v, con reglas al estilo de las de composición. Se prueba la confluencia débil sobre términos abiertos. Como aplicación de lo anterior, se puede dar un cálculo simplificado, derivado de lambda v, que usa un solo índice de de Bruijn, el cual es un sub cálculo del anterior y con las mismas propiedades. Se demuestra luego la normalización débil del cálculo lambda Se simplemente tipado sobre términos abiertos, en donde las abstracciones se decoran con tipos, y las meta variables, índices de de Bruijn y operadores de actualización se decoran con contextos. La prueba se basa en el cálculo Lambda omega e, que sobre términos semi-abiertos (i.e. aquellos que admiten variables de término pero no de sustitución) es isomorfo a Lambda Se sobre términos abiertos. Esta prueba está fuertemente influenciada por otra previa de normalización débil para el cálculo lambda sigma simplemente tipado pero con diferencias substanciales que indican que los dos estilos requieren distinto tratamiento. Además, introducimos el cálculo lambda omega e, sub cálculo de lambda omega e, el cual usa sólo un índice de de Bruijn, con lo que es más cercano a lambda sigma que lambda omega e. Para lambda omega'e tipado probamos también la normalización débil sobre términos tipados semi-abiertos. Presentamos una extensión del cálculo lambda (nu) que incluye un constructor de casos primitivo que se propaga a través de las abstracciónes como una sustitución lineal de cabeza antes de actuar sobre los constructores, y probamos que este modo de descomposición del apareamiento de patrones permite recuperar la expresividad del estilo de los patrones de ML. Se demuestra que este sistema satisfase confluencia, usando una técnica de "dividir y conquistar" semi automática por al cual se determinan todo los pares de sub sistemas de este cálculo que conmutan (considerando todas las combinaciones de las nueve reglas de reducción). Finalmente, se prueba un teorema de separación (débil) para todo el formalismo, usando una técnica de separación inspirada en la técnica Böhm-out. Por último, como otra faceta de exploración de sub cálculos, analizamos los términos que se satisfacen la propiedad de expandir a términos puros, para lambda v y lambda S. Probamos que estos conjuntos de términos con propios yu no recursivos. Como aplicación, se prueba la imposibilidad de mapeos adecuados entre ciertos pares de cálculos.

Abstract:
This thesis is about some problems on rewriting theory and explicit substitution calculi. The main topic is the study of sub-calculi for several rewriting systems. After a biased introduction to rewriting, lambda-calculus and explicit substitution, we make a compatative study of the mail rewriting formalisms, identifying a hierarchy between them. As a first approach to new calculi, we address Revesz'lambda-calculus with names, involving four rewriting rules, with the particularity that it does not have any substitution at all. We show the relative soundness and the confluence. We also propose and study two versions using de Bruijn indices, proving that all these properties are preserved. We then move to perpetuality in the lambda v explicit substitution calculus, and study perpetual rewrite strategies, i.e. those strategies that preserve the possibility of infinite derivarions. We give as an application a set of deterministic inference rules wich characterize inductively the subsystem of strongly normalizing terms, and we present an effective perpetual reduction strategy for lambda v. Then we study different extensions of lambda v-calculus, with the addition of composition-like rules. Weak confluence on open terms is proved. As an application, a derived simplification of lambda v with a unique de Bruijn index can be given, which is a sub-calculus of the former and has the same properties. We show the weak normalization of the simply-typed lambda Se-calculus with open terms where abstractions are decorated with types, and meta-variables, de Bruijn indices and updating operators are decorated whit environments. The proof is based on the lambda omega e-calculus, a calculus wich over semi-open terms (i.e. those wich allow term variables but not substitution variables) is isomorphic to lambda Se, over open terms. This proof is strongly influenced by a previous proof of weak normalization for the simply-typed lambad sigma-calculus but with subtle differences which show that the two styles require different attention. Ferthermore, we give a new calculus, lambda omega'e, sub-calculus of lambda omega e, which handles a unique de Bruijn index, which is then closer to lambda sigma than lambda omega e. For lambda omega'e we also prove the weak normalization for typed semi-open terms. We present an extension of the lambda nu-calculus with a primitive case construct that propagares through abstractions like a head linear substitution before doing constructor substitution, and show that this way of decomposing pattern matching allows to recover the expressiveness of ML-style pattern matching. Then we prove that this system enjoys confluence using a semi-automatic "divide and conquer" technique by wich we determine all the pairs of commuting subsystens of the fornalism (considering all the possible combinations of the nine reduction rules). Finally, we prove a (weak) separation theorem for the whole formalism, using a separation technique inspired by the Bóhm-out technique. And, as another facet of sub-calculi exploration, we inverstigate the terms wich satisfy the property of expansion to pure terms, for lambda v and lambad S. We prove that these sets of terms are proper and non-recursive. As an application, we prove the impossibility id adequate mapping between certain pairs of calculi.

Gorín, Daniel Alejandro. "Técnicas de razonamiento automático para lógicas híbridas" (2009) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
Las "lógicas híbridas" extienden a las lógicas modales tradicionales con el poder de describir y razonar sobre cuestiones de identidad, lo cual es clave para muchas aplicaciones. Aunque lógicas modales que hoy llamaríamos "híbridas" pueden rastrearse hasta cuatro décadas atrás, su estudio sistem ático data de fines de la década del '90. Parte de su interés proviene de que llenan un hueco de expresividad importante de las lógicas modales tradicionales. Uno de los temas de esta tesis es el problema de la satisfacibilidad para la lógica híbrida más conocida, denominada H(@;!), y algunas de sus sublógicas. El de la satisfacibilidad es el problema fundamental en razonamiento automático. En el caso de las lógicas híbridas, éste se ha estudiado fundamentalmente a partir del método de tableaux. En esta tesis intentamos completar el panorama del área investigando el problema de la satisfacibilidad para lógicas híbridas usando resolución clásica de primer orden (vía traducciones) y variaciones de un cálculo basado en resolución que opera directamente sobre fórmulas híbridas. Presentamos, en primer lugar, traducciones de complejidad lineal de fórmulas de H(@;!) a lógica de primer orden, que preservan satisfacibilidad. Éstas están concebidas de manera de reducir el espacio de búsqueda de un demostrador automático basado en resolución de primer orden. Luego cambiamos nuestra atención a cálculos que operan directamente sobre fórmulas híbridas. En particular, consideramos el cálculo llamado de"resolución directa". Inspirados por el caso clásico, transformamos este cálculo en uno de resolución ordenada con funciones de selección y probamos que posee la "propiedad de reducción de contraejemplos", de lo cual se deduce que es completo y compatible con el criterio de redundancia estándar. Mostramos también que un refinamiento de este cálculo es un método de decisión para la sublógica decidible H(@). En la última parte de esta tesis, consideramos ciertas formas normales para lógicas híbridas y otras lógicas modales extendidas. En particular nos interesan formas normales donde se garantice que ciertas modalidades no aparecen por debajo de otros operadores modales. Este tipo de transformaciones puede ser aprovechadas en una etapa de preprocesamiento a fin de reducir el número de inferencias requeridas por un demostrador modal. Al intentar expresar estos resultados de extractibilidad de una manera que comprenda también otras lógicas modales extendidas, llegamos a una formulación de la semántica modal basada en un tipo novedoso de modelos definidos de manera coinductiva. Muchas lógicas modales extendidas (incluyendo las lógicas híbridas) pueden verse en términos de clases de modelos coinductivos. De esta manera, resultados que antes debían probarse por separado para cada lenguaje (pero cuyas pruebas eran en general rutinarias) pueden establecerse de manera general.

Abstract:
Hybrid logics augment classical modal logics with machinery for describing and reasoning about identity, which is crucial in many settings. Although modal logics we would today call "hybrid" can be traced back to the work of Prior in the 1960's, their systematic study only began in the late 1990's. Part of their interest comes from the fact they fill an important expressivity gap in modal logics. In fact, they are sometimes referred to as "modal logics with equality". One of the unifying themes of this thesis is the satisfiability problem for the arguably best-known hybrid logic, H(@; !), and some of its sublogics. Satisfiability is the basic problem in automated reasoning. In the case of hybrid logics it has been studied fundamentally using the tableaux method. In this thesis we attempt to complete the picture by investigating satisfiability for hybrid logics using first-order resolution (via translations) and variations of a resolution calculus that operates directly on hybrid formulas. We present firstly several satisfiability-preserving, linear-time translations from H(@; !) to first-order logic. These are conceived in a way such that they tend to reduce the search space of a resolution-based theorem prover for first-order logic. notations can be safely ignored. We then move our attention to resolution-based calculi that work directly on hybrid formulas. In particular, we will consider the so-called direct resolution calculus. Inspired by first-order logic resolution, we turn this calculus into a calculus of ordered resolution with selection functions and prove that it possesses the reduction property for counterexamples from which it follows its completeness and that it is compatible with the well-known standard redundancy criterion. We also show that certain refinement of this calculus constitutes a decision procedure for H(@), a decidable fragment of H(@; !). In the last part of this thesis we investigate certain normal forms for hybrid logics and other extended modal logics. We are interested in normal forms where certain modalities can be guaranteed not to occur under the scope of other modal operators. We will see that these kind of transformations can be exploited in a pre-processing step in order to reduce the number of inferences required by a modal prover. In an attempt to formulate these results in a way that encompasses also other extended modal logics, we arrived at a formulation of modal semantics in terms of a novel type of models that are coinductively defined. Many extended modal logics (such as hybrid logics) can be defined in terms of classes of coinductive models. This way, results that had to be proved separately for each difierent language (but whose proofs were known to be mere routine) now can be proved in a general way.

Mera, Sergio Fernando. "Lógicas modales con memoria" (2009) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
Desde la antigüedad hasta hoy, el campo de la lógica ha ido ganando fuerza y actualmente contribuye activamente en muchas áreas distintas, como filosofía, matemática, lingüística, ciencias de la computación, inteligencia artificial, fabricaci ón de hardware, etc. Cada uno de estos escenarios tiene necesidades espec íficas, que van desde requerimientos muy concretos, como un método de inferencia eficiente, hasta propiedades teóricas más abstractas, como un sistema axiomático elegante. Durante muchos años, los lenguajes clásicos (principalmente la lógica de primer orden) eran la alternativa a utilizar, pero esta gran variedad de aplicaciones hizo que otro tipo de lógicas empezaran a resultar atractivas en muchas situaciones. Supongamos que llega el momento de elegir una lógica para una tarea en particular. ¿Cómo podemos decidir cuál es la más adecuada? ¿Qué propiedades deberíamos buscar? ¿Cómo podemos "medir" una lógica con respecto a otras? Éstas no son preguntas sencillas, y no hay una receta general que uno pueda seguir. En esta tesis vamos a restringir estas cuestiones a una familia de lógicas en particular, y en ese contexto vamos a investigar algunos aspectos teóricos que nos van a ayudar a responder parte de estas inquietudes. Podemos aprender mucho estudiando casos particularmente interesantes, y nuestra contribución se va a desarrollar teniendo esa filosofía en mente. Las lógicas modales proposicionales ofrecen una alternativa a los lenguajes tradicionales. Pueden ser pensadas como un conjunto de herramientas que permiten diseñar lógicas específicamente construidas para una tarea en particular, posibilitando tener un control fino en su expresividad. Más aún, las lógicas modales resultaron tener un buen comportamiento computacional que probó ser bastante robusto frente a extensiones. Estas características, entre otras, ubicaron a las lógicas modales como una alternativa atractiva con respecto a los lenguajes clásicos. En este trabajo vamos a presentar una nueva familia de lógicas modales llamada memory logics. Las lógicas modales tradicionales posibilitan describir estructuras relacionales desde una perspectiva local, ¿pero cuál será el resultado si permitimos que una fórmula cambie la estructura en la que está siendo evaluada? Queremos explorar el efecto de agregar a las lógicas modales clásicas una estructura de almacenamiento explícita, una memoria, que permita modelar comportamiento dinámico a través de operadores que permitan almacenar y recuperar información de la memoria. Naturalmente, dependiendo del tipo de estructura de almacenamiento que utilicemos, y de qué operadores tengamos disponibles, la lógica resultante va a tener distintas propiedades que valen la pena investigar. Esta tesis está organizada de la siguiente manera. En el Capítulo 1 empezamos dando un breve resumen de cómo nacieron las lógicas modales, mostrando las diferentes perspectivas con las que históricamente se miró a la lógica modal. Luego presentamos formalmente a la lógica modal básica, y a un conjunto extendido de operadores que permiten apreciar el "estilo" modal de algunos lenguajes más ricos. Este capítulo ánaliza con un primer bosquejo de las memory logics, mostrando cómo pueden ayudar a modelar la noción de estado cuando dejamos a un conjunto como estructura de almacenamiento. El capítulo 2 está dedicado a presentar a las memory logics con detalle. En dicho capítulo mostramos algunos ejemplos que pueden ser descriptos agregando un conjunto a las estructuras relacionales estándar, junto con los operadores usuales sobre conjuntos que permiten agregar elementos y verificar pertenencia. A continuación mostramos otros operadores sobre conjuntos que pueden ser considerados, y discutimos la posibilidad de agregar restricciones a la interacción entre los operadores que trabajan sobre la memoria y los operadores modales. Estas restricciones pueden ser pensadas como una manera de lograr un control más úno en la expresividad. Dado que realizamos cambios en las lógicas modales clásicas, estamos interesados en analizar el impacto que esos cambios causaron en las lógicas resultantes. Por lo tanto, el resto del capítulo presenta un conjunto de herramientas a través de las cuales analizamos esta nueva familia de lógicas. Este conjunto de herramientas puede verse como un esquema que organiza el resto de la tesis, y que permite analizar a las memory logics en téerminos de expresividad, complejidad, interpolación y teoría de prueba. El resto de los capítulos investigan cada uno de estos aspectos en detalle. En los Capítulos 3 y 4 exploramos el poder expresivo de varias memory logics y estudiamos para cada fragmento la decidibilidad del problema de determinar la satisfactibilidad de una fórmula. En los casos decidibles, determinamos la complejidad computacional de cada uno. Analizamos el impacto de los diferentes operadores, su interacción, y también estudiamos otras estructuras de almacenamiento, como la pila. Luego, en el Capítulo 5, analizamos las propiedades de interpolación de Craig y definibilidad de Beth para algunas memory logics. También nos interesa estudiar a las memory logics desde la perspectiva de la teoría de prueba. En los Capítulos 6 y 7 nos volcamos al estudio de axiomatizaciones á la Hilbert y sistemas de tableau, y caracterizamos varios fragmentos usando principalmente técnicas utilizadas en lógicas híbridas. En el Capítulo 8 presentamos nuestras conclusiones, mencionamos algunos problemas abiertos y futuras direcciones de investigación.

Abstract:
From ancient times to the present day, the field of logic has gained significant strength and now it actively contributes to many different areas, such as philosophy, mathematics, linguistic, computer science, artificial intelligence, hardware manufacture, etc. Each of these scenarios has specific needs, that range from very concrete requirements, like an efficient inference method, to more abstract theoretical properties, like a neat axiomatic system. Given this wide diversity of uses, a motley collection of formal languages has been developed. For many years, classical languages (mainly classical first order logic) were the alternative, but this assortment of applications made other types of logics also attractive in many situations. Imagine that the time for choosing a logic for some specific task arrives. How can we decide which is the one that fits best? Which properties should we look for? How can we "measure" a logic with respect to others? These are not easy questions, and there is not a general recipe one can follow. In this thesis we are just going to restrict these questions to a particular family of logics, and in that context we will investigate theoretical aspects that help to answer some of these concerns. Much can be discovered by carefully analyzing appealing cases, and our contribution will be developed having that philosophy in mind. Propositional modal logics offer an alternative to traditional languages. They can be regarded as a set of tools that allow to design logics specially tailored for specific tasks, having a fine-grained control on their expressivity. Additionally, modal logics turned out to have a good computational behavior, which proved to be quite robust under extensions. These characteristics, among others, placed modal logics as an attractive alternative to classical languages. In this dissertation we are going to present a new family of modal logics called memory logics. Traditional modal logics enable us to describe relational structures from a local perspective. But what about changing the structure? We want to explore the addition of an explicit storage structure to modal logics, a memory, that allows to model dynamic behavior through explicit memory operators. These operators store or retrieve information to and from the memory. Naturally, depending on which type of storage structure we want, and which memory operators are available, the resulting logic will enjoy different properties that are worth investigating. The thesis is organized as follows. In Chapter 1 we start by giving a brief recap of how modal logic was born, showing the different historical perspectives used to look at modal logic. Then we formally present the basic modal logic and a set of extended operators that helps grasp the modal "flavor" of some richer languages. We finish this chapter by giving a first glance of memory logics, and showing how they can help to model state when we choose to use a set as storage structure. Chapter 2 is devoted to present memory logics in detail. We show some examples that can be described by adding a set to standard relational structures, and the usual set operators to add elements and test membership. We then show some other memory operators that can be considered, and we discuss the possibility of adding constraints to the interplay between memory and modal operators. These constraints can be regarded as a way to have a finer-grained control on the logic expressivity. Since we have made changes to classical modal logics, we are interested in analyzing the impact those changes cause in the resulting logics. Therefore, the rest of this chapter presents a basic logic toolkit through which we can analyze this new family of logics. This toolkit can be seen as an outline that organizes the rest of the thesis and that allows to analyze memory logics in terms of expressivity, complexity, interpolation and proof theory. The rest of the chapters investigate each of these aspects in detail. In Chapters 3 and 4 we explore the expressive power of several memory logics and we study the decidability of their satisfiability problem. In the decidable cases, we determine their computational complexity. We analyze the impact of the different memory operators we consider, and how they interact. We also study other memory containers, such as a stack. Then, in Chapter 5, we analyze Craig interpolation and Beth definability for some memory logic fragments. We also study memory logics from a proof-theoretic perspective. In Chapter 6 and 7 we turn to Hilbert-style axiomatizations and tableau systems, and we characterize several fragments of the memory logic family mostly using techniques borrowed from hybrid logics. We close in Chapter 8 with some concluding remarks, open problems and directions for further research.

Ponzio, Pablo Daniel. "Cómputo secuencial eficiente de cotas ajustadas, y su impacto en la performance de los análisis de programas basados en SAT" (2014-06-13) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
Dada una descripción formal de los estados válidos del heap -por ejemplo, un invariante de una estructuras de datos- las cotas ajustadas para los campos del heap son el conjunto de los valores que pueden tomar los campos en alguna instancia válida. Así, los valores de campos que no pertenecen a las cotas ajustadas pueden ser ignorados por los análisis automáticos (acotados) de código, reduciendo así el espacio de estados a explorar, y mejorando la performance del análisis. Sin embargo, el cómputo de cotas ajustadas es costoso. El único enfoque conocido que computa estas cotas en un tiempo aceptable, TACO+, es intrínsecamente paralelo, y requiere de un cluster con varias computadoras para su ejecución eficiente. En este trabajo se aborda el problema de computar eficientemente cotas ajustadas en entornos de ejecución secuenciales. Así, se presentan dos nuevos enfoques para resolver este problema. El primero, denominado bottom-up, utiliza un procedimiento de decisión basado en SAT para visitar instancias válidas del heap, y computa cotas ajustadas usando los valores de los campos de estas instancias. bottom-up, al igual que TACO+, requiere de una especificación en algún lenguaje declarativo de alto nivel -como JML para JAVA- de los estados válidos del heap. De esta manera, bottom-up y TACO+ generan cotas ajustadas equivalentes. El segundo, SLBD, se basa en una especificación del heap en términos de un predicado inductivo de la lógica de separación. Este enfoque computa cotas ajustadas mientras realiza (un número finito de) desplegados del predicado inductivo de entrada. En algunos casos SLBD puede producir cotas ajustadas diferentes a las de TACO+ (y bottom-up). Se evaluaron experimentalmente los enfoques bottom-up, SLBD y la técnica relacionada TACO+, en la generación de cotas ajustadas para varias clases contenedoras JAVA. Los resultados muestran que, en un ambiente de ejecución secuencial, bottom-up es un orden de magnitud más rápido que TACO+ (secuencializado), y que SLBD es dos órdenes de magnitud más rápido que bottom-up. Además, se evaluó el impacto de las cotas ajustadas generadas por nuestros enfoques en la veri ficación de código y en la generación exhaustiva de estructuras (que satisfacen un predicado) basados en SAT. Los resultados indican que los enfoques que computan cotas ajustadas secuencialmente (vía bottom-up o SLBD), y luego las aprovechan durante el análisis, son significativamente más eficientes que los análisis convencionales, que no explotan la idea de cotas ajustadas. Además, para los análisis basados en SAT mencionados, los resultados muestran que las cotas ajustadas computadas por SLBD tienen un impacto similar a las computadas por TACO+ y bottom-up.

Abstract:
Given a formal description of the feasible heap states -for example, an invariant for a data structure-, tight field bounds for heap fields are the set of values that the fields can take in any valid instance. Thus, field values that do not belong to the tight field bounds can be safely ignored by automated (bounded) program analyses, reducing the state space to be explored, and improving the performance of the analysis. However, computing tight field bounds is an expensive process. The only known approach to compute these bounds that performs reasonably, TACO+, is intrinsically parallel, and it requires a cluster of several computers to run efficiently. In this work we address the problem of computing tight field bounds efficiently under a secuential execution environment. Thus, we introduce two novel approaches to solve this problem. The first, called bottom-up, uses a SAT based decision procedure to traverse valid heap instances, and computes tight field bounds using the field values of the visited instances. bottom-up, like TACO+, requires a description of the feasible heap states in a high level declarative language -like JML for JAVA-. In this way, bottom-up and TACO+ yield equivalent tight field bounds. The second, SLBD, is based on a specification of the valid heap states in terms of a separation logic's inductive predicate. This approach computes tight field bounds during the process of unfolding its input's inductive predicate (a finite number of times). In some cases, the tight field bounds computed by SLBD and TACO+ (and bottom-up) might differ. We assessed bottom-up, SLBD and the related technique TACO+ experimentally, in generating tight field bounds for several JAVA container classes. The results show that, under a secuential execution environment, bottom-up is an order of magnitude faster than TACO+ (secuentialized), and that SLBD is two orders of magnitude faster than bottom-up. Moreover, we assesed the impact of the tight field bounds produced by our approaches in SAT based code analysis and in exhaustive bounded generation of structures (satisfying a predicate). The results show that the approaches that compute tight field bounds secuentially (via bottom-up or SLBD), and subsecuently exploit them during analysis, are significatively faster than the more conventional analyses that do not take advantage of tight field bounds. Furthermore, for the aformentioned SAT based analyses, the experiments show that the tight field bounds computed by SLBD have a similar impact to those computed by TACO+ and bottom-up.

http://digital.bl.fcen.uba.ar

Biblioteca Central Dr. Luis Federico Leloir - Facultad de Ciencias Exactas y Naturales - Universidad de Buenos Aires
Intendente Güiraldes 2160 - Ciudad Universitaria - Pabellón II - C1428EGA - Tel. (54 11) 4789-9293 int 34