1,720,987 research outputs found
Summary-based inference of quantitative bounds of live heap objects
Full text linkThis article presents a symbolic static analysis for computing parametric upper bounds of the number of simultaneously live objects of sequential Java-like programs. Inferring the peak amount of irreclaimable objects is the cornerstone for analyzing potential heap-memory consumption of stand-alone applications or libraries. The analysis builds method-level summaries quantifying the peak number of live objects and the number of escaping objects. Summaries are built by resorting to summaries of their callees. The usability, scalability and precision of the technique is validated by successfully predicting the object heap usage of a medium-size, real-life application which is significantly larger than other previously reported case-studies.Fil: Braberman, Victor Adrian. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Garbervetsky, Diego David. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Hym, Samuel. Universite Lille 3; FranciaFil: Yovine, Sergio Fabian. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentin
Enabledness-based program abstractions for behavior validation
Full text linkCode artifacts that have nontrivial requirements with respect to the ordering in which their methods or procedures ought to be called are common and appear, for instance, in the form of API implementations and objects. This work addresses the problem of validating if API implementations provide their intended behavior when descriptions of this behavior are informal, partial, or nonexistent. The proposed approach addresses this problem by generating abstract behavior models which resemble typestates. These models are statically computed and encode all admissible sequences of method calls. The level of abstraction at which such models are constructed has shown to be useful for validating code artifacts and identifying findings which led to the discovery of bugs, adjustment of the requirements expected by the engineer to the requirements implicit in the code, and the improvement of available documentation.Fil: de Caso, Guido. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Braberman, Victor Adrian. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Garbervetsky, Diego David. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Uchitel, Sebastian. Universidad de Buenos Aires; Argentina. Imperial College London; Reino Unido. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentin
TacoFlow: optimizing SAT program verification using dataflow analysis
Full text linkIn previous work, we presented TACO, a tool for efficient bounded verification. TACO translates programs annotated with contracts to a SAT problem which is then solved resorting to off-the-shelf SAT-solvers. TACO may deem propositional variables used in the description of a program initial states as being unnecessary. Since the worst-case complexity of SAT (a known NP problem) depends on the number of variables, most times this allows us to obtain significant speed ups. In this article, we present TacoFlow, an improvement over TACO that uses dataflow analysis in order to also discard propositional variables that describe intermediate program states. We present an extensive empirical evaluation that considers the effect of removing those variables at different levels of abstraction, and a discussion on the benefits of the proposed approach.Fil: Cuervo Parrino, Bruno. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; ArgentinaFil: Galeotti, Juan Pablo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Universitat Saarland; AlemaniaFil: Garbervetsky, Diego David. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Frias, Marcelo Fabian. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Instituto Tecnológico de Buenos Aires. Facultad de Ingeniería. Departamento de Informática; Argentin
Integrated program verification tools in education
Full text linkAutomated software verification is an active field of research, which has made enormous progress both in theoretical and practical aspects. Even if not ready for large-scale industrial adoption, the technology behind automated program verifiers is now mature enough to gracefully handle the kind of programs that arise in introductory programming courses. This opens exciting new opportunities in teaching the basics of reasoning about program correctness to novice students. However, for these tools to be effective, command-line-style user-interfaces need to be replaced. In this paper, we report on our experience using the verifying compiler for PEST in an introductory programming course as well as in a more advanced course on program analysis. PEST is an extremely basic programming language, but with expressive annotations capabilities and semantics amenable to verification. In particular, we comment on the crucial role played by the integration of this verifying compiler with the Eclipse integrated development environment.Fil: de Caso, Guido. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Garbervetsky, Diego David. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Gorin, Daniel Alejadro. Friedrich Alexander Universität; Alemania. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentin
Enabledness-based Testing of Object Protocols
No full textA significant proportion of classes in modern software introduce or use object protocols, prescriptions on the temporal orderings of method calls on objects. This article studies search-based test generation techniques that aim to exploit a particular abstraction of object protocols (enabledness preserving abstractions (EPAs)) to find failures. We define coverage criteria over an extension of EPAs that includes abnormal method termination and define a search-based test case generation technique aimed at achieving high coverage. Results suggest that the proposed case generation technique with a fitness function that aims at combined structural and extended EPA coverage can provide better failure-detection capabilities not only for protocol failures but also for general failures when compared to random testing and search-based test generation for standard structural coverage.Fil: Godoy, Javier Ignacio. Universidad Nacional de General Sarmiento; ArgentinaFil: Galeotti, Juan Pablo. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Garbervetsky, Diego David. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Uchitel, Sebastian. Consejo Nacional de Investigaciones Científicas y Técnicas. Oficina de Coordinación Administrativa Ciudad Universitaria. Instituto de Investigación en Ciencias de la Computación; Argentin
An Empirical Study on How Sapienz Achieves Coverage and Crash Detection
No full textSeveral tools for automatically testing Android applications have been proposed. In particular, Sapienz is a search-based tool that has been recently deployed in an industrial setting. Although it has been shown that Sapienz outperforms several state-of-the-art tools, it is still to be seen what features of SAPIENZ impact the most on its effectiveness. We conducted an extensive empirical study where we compare the impact of the search algorithm and the usage of motif genes, a more compact representation of individuals. Our empirical study shows that the usage of motif genes improves coverage both for Evolutionary Algorithms and random approaches. In particular, it also shows that NSGA-II, the multi-objective evolutionary algorithm used by Sapienz, does not have a clear improvement over other algorithms. In terms of number of crashes detected, our study shows that both NSGA-II and Random Search perform similarly. While the usage of motif genes improves the crash detection of algorithms, it is not enough to make it statistically significant. These facts cast doubts about the use of Evolutionary Algorithms in the context of Android test generation and suggest that motif genes can have a great impact on the overall effectiveness.Fil: Arcuschin, Iván. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; ArgentinaFil: Galeotti, Juan Pablo. Consejo Nacional de Investigaciones Científicas y Técnicas. Oficina de Coordinación Administrativa Ciudad Universitaria. Instituto de Investigación en Ciencias de la Computación. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Instituto de Investigación en Ciencias de la Computación; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; ArgentinaFil: Garbervetsky, Diego David. Consejo Nacional de Investigaciones Científicas y Técnicas. Oficina de Coordinación Administrativa Ciudad Universitaria. Instituto de Investigación en Ciencias de la Computación. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Instituto de Investigación en Ciencias de la Computación; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentin
A Corralando EPAs : acercando el modelo mental al computacional
No full textLa congestión en las grandes ciudades y en áreas sobrepobladas es uno de los mayores desafíos en la logística urbana, y hoy en día se ha convertido en uno de los inconvenientes principales en el planeamiento urbano y la denominada distribución de la última milla debido a su impacto económico, social y ambiental. La mayor parte de la investigación dedicada a los Problemas de Ruteo de Vehículos (VRP, por su sigla en inglés) considera que el tiempo de viaje entre dos sitios cualesquiera es constante a lo largo del horizonte de planeamiento. En los últimos años, ha habido una tendencia a enriquecer estos modelos mediante la incorporación de funciones de tiempo de viaje más complejas que capturen el efecto de la congestión, conocidos como VRP Dependientes del Tiempo (TDVRP, ver Gendreau et al. [11])). La incorporación explícita de la congestión a nivel táctico es un aspecto fundamental de los Sistemas de Soporte a la Decisión (DSS) modernos a fin de obtener planificaciones y recorridos que sean representativos de las operaciones habituales (Huang et al. [15]). Sin embargo, los algoritmos presentes actualmente en la literatura requieren mejoras, como se muestra en Dabia et al. [6] y Montero et al. [26], para poder transformarse en herramientas automatizadas que puedan ser utilizadas en la práctica. Los enfoques exactos generales para las variantes monovehículo suelen basarse en modelos de Programación Lineal Entera (PLEM) y algoritmos Branch&Cut (B&C), como puede verse en los trabajos de Cordeau et al. [5] para el Problema del Viajante de Comercio Dependiente del Tiempo (TDTSP) y Arigliano et al. [3] para el TDTSP-TW, es decir, el TDTSP con ventanas de tiempo. Los algoritmos exactos para problemas multivehículos suelen recurrir a modelos de PLEM combinados con técnicas de descomposición, dando lugar a los denominados algoritmos Branch&Price (B&P). Uno de los ingredientes principales de estos algoritmos radica en la resolución del subproblema de generación de columnas, que puede ser formulado como un problema de Camino Mínimo Elemental Dependiente del Tiempo con Restricciones de Recursos y Beneficios (TD-PESPPRC). Dabia et al. [6] siguen este enfoque y proponen un algoritmo B&P para el TDVRP con Ventanas de Tiempo (TDVRP-TW), que es luego adaptado por Sun et al. [29] para considerar también restricciones de precedencia. En ambos artículos, en sus problemas correspondientes es abordado mediante algoritmos de labeling y Programación Dinámica (DP). La generación de columnas aparece como un problema difícil y desafiante computacionalmente, especialmente cuando no se posee un recurso limitante (por ejemplo, la capacidad o las ventanas de tiempo) que permita reducir de forma significativa el espacio de búsqueda. En esta tesis abordamos el TD-PESPPRC con restricciones de capacidad pero, a diferencia de los enfoques anteriores, no consideramos la presencia de ventanas de tiempo en los clientes. Desde el punto de vista práctico, con esta configuración los algoritmos de labeling propuestos previamente encuentran fuertes limitaciones dado que el espacio de búsqueda se vuelve muy grande, dando lugar también a la construcción de rutas con muchos clientes como parte de las soluciones al problema. Luego, la importancia de estudiar esta variante tiene dos razones principales. La primera de ellas es que las versiones mono-vehículo, como el TDTSP y el TDTSP-TW, pueden ser fácilmente adaptadas introduciendo pequeñas modificaciones al modelo. En segundo lugar, la obtención de un algoritmo eficiente para el TD-PESPPRC abriría la posibilidad a integrarlo en los esquemas B&P en los casos donde los enfoques tradicionales no son satisfactorios. Con esto en mente, proponemos un modelo PLEM mejorado basado en el propuesto por Sun et al. [29]. Realizamos un estudio teórico enfocado en derivar nuestras familias de desigualdades válidas que exploten la estructura particular introducida por la red subyacente dependiente del tiempo, y que permita mejorar la calidad de las cotas inferiores provistas por la relajación lineal del modelo. Estas familias son embebidas en un algoritmo de tipo Branch&Cut, que es evaluado experimentalmente en función del tiempo de cómputo requerido y la calidad de las cotas provistas. Los resultados son muy prometedores y muestran que el algoritmo es capaz de resolver instancias de 25 vértices consistentemente dentro de los l ́ımites establecidos, que los resultados teóricos pueden ser extendidos a otras variantes de problemas dependientes del tiempo y que el enfoque en su totalidad tiene potencial de ser aplicado en la práctica.Congestion in large cities and populated areas is one of the major challenges in urban logistics, becoming one of the key issues in city planning and last-mile logistics due to its economic, social and environmental impact. Most of the research devoted to the Vehicle Routing Problem (VRP) considers that travel times between any two locations are fixed along the time horizon. In the last few years, there has been a trend to enrich these models by incorporating more complex travel time functions to capture the effect of congestion, known as Time-Dependent VRPs (TDVRP, see, e.g., Gendreau et al. [11], for an updated survey). Incorporating the congestion explicitly at a tactical level is a key aspect of modern Decision Support Systems (DSS) in order to obtain distribution plans that are representative of the real-life operations (Huang et al. [15]). However, state-of-the-art algorithms require further developments, as shown in Dabia et al. [6] and Montero et al. [26], in order to derive them into automated tools that can be implemented in practice. Standard exact approaches for single-vehicle problems are generally addressed by means of Integer Linear Programming (ILP) and Branch&Cut (B&C) algorithms, as shown in Cordeau et al. [5] for the Time Dependent Traveling Salesman Problem (TDTSP) and by Arigliano et al. [3] for the TDTSP with Time Windows (TDTSP-TW). Exact approaches for multi-vehicle variants generally resort to ILP combined with decomposition techniques, resulting in Branch&Price (B&P) algorithms. One of the key ingredients of the latter rely on the pricing problem within the column generation algorithm, which can be formulated as a Time-Dependent Elementary Shortest Path Problem with Resource Constraints and Profits (TD-PESPPRC). Dabia et al. [6] follow this approach and propose a B&P algorithm for the capacitated TDVRP with time windows (TDVRP-TW), which is later adapted by Sun et al. [29] to further consider the TD-PESPPRC with precedence constraints. In both papers, the corresponding problem is tackled by labeling and Dynamic Programming (DP) algorithms. The pricing step appears as a very difficult and challenging problem that requires further developments, specially under the absence of a limiting resource (for instance, time windows) that may allow to reduce the search space. In this thesis, we tackle the TD-PESPPRC with capacity constraints but, opposed to the previously mentioned cases, we do not consider time windows. From a practical standpoint, under these settings the standard labeling algorithms from previous approaches find some limitations since the search space becomes too large to explore, giving place to constructing large routes as part of the overall solution. Therefore, the importance of studying this variant has two main reasons. Firstly, single-vehicle variants, such as the TDTSP and the TDTSP-TW, are easily recovered with some minor modifications to the formulation. Secondly, an efficient algorithm for the TD-PESPPRC could be integrated within a B&P scheme where the standard approaches are not satisfactory. For this purpose, we propose an enhanced ILP formulation based on the one proposed in Sun et al. [29]. We perform a theoretical study focused on deriving three new families of valid inequalities that exploit the particular structure introduced by the time-dependent underlying network aiming to improve the quality of the lower bounds provided by the LP relaxation. These families are embedded in a Branch&Cut algorithm, which is experimentally evaluated in terms of computing times and quality of the lower bounds. The results are very promising, showing that our algorithm is able to solve consistently instances with 25 vertices in reasonable computing times, that the results can be extended to other time-dependent problems and that the overall approach has potential to be applied in practice.Fil: Lera Romero, Leandro. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina
Static analysis of .NET programs.
No full textEn esta tesis presentamos el diseño e implementación de una amplia gama de análisis estáticos para la plataforma .NET, con foco en la escalabilidad. Nos concentramos en .NET dada su gran popularidad en la industria y el amplio conjunto de características que provee, pertenecientes a los paradigmas orientado a objetos y funcional, incluyendo programación concurrente y la manipulación de bajo nivel de punteros. La combinación de todas estas características hacen del análisis estático un desafío. Por un lado, presentamos un framework de análisis estático distribuido de programa completo, diseñado para escalar con el tamaño de la entrada. Nuestro enfoque está basado en el modelo de programación con actores para ser ejecutado en la nube. Nuestra decisión de utilizar una red de computadoras en la nube provee un grado de elasticidad para recursos de CPU, memoria y almacenamiento. Para demostrar el potencial de nuestra técnica, mostramos cómo puede ser implementado un análisis de call graph típico en una configuración distribuida. Además, extendemos nuestro análisis para soportar actualizaciones incrementales del código fuente y mostramos cómo los resultados computados previamente pueden ser actualizados sin tener que volver a calcularlos de cero. Por otro lado, presentamos un framework de análisis estático de programas y herramientas específicamente diseñado para la plataforma .NET. Este framework provee muchas funcionalidades, incluyendo algunas representaciones intermedias como el código de tres direcciones, adecuado para la implementación de un análisis estático, así como también provee una amplia gama de análisis y transformaciones como son la inferencia de tipos, los análisis de control-flow y data-flow, y la construcción de call graph y points-to graph, entre otros. No sabemos de ningún otro framework de análisis estático de código públicamente disponible para la comunidad .NET que provea este tipo de funcionalidades. Para demostrar las capacidades de nuestro framework, presentamos también algunas aplicaciones cliente que aprovechan sus funcionalidades, como un análisis de optimización de consultas Big Data para detectar automáticamente columnas no utilizadas y dependencias entre tablas de entrada y salida de operadores definidos por el usuario desarrollados en algún lenguaje de la plataforma .NET como C#.In this thesis we present the design and implementation of a wide range of static analyses for the .NET platform, with focus in scalability. We target .NET given its popularity in the industry and the rich set of features it provides, ranging from object-oriented to functional paradigms, including concurrent programming and low-level pointer manipulation. The combination of all these features make static analysis very challenging. On the one hand, we present a distributed, whole-program static analysis framework that is designed to scale with the size of the input. Our approach is based on the actor programming model and is deployed in the cloud. Our reliance on a cloud cluster provides a degree of elasticity for CPU, memory and storage resources. To demonstrate the potential of our technique, we show how a typical call graph analysis can be implemented in a distributed setting. In addition, we extend our analysis to support incremental source code updates and show how the previously computed results can be updated without having to recompute them from scratch. On the other hand, we present a static program analysis framework and tools specifically designed for the .NET platform. It provides many features, including a few intermediate code representations such as a three-address code suitable for implementing a static analysis on top of it, and a rich set of analyses and transformations such as type inference, control-flow and data-flow analyses, and call graph and points-to graph construction, among others. We don’t know of any other static analysis framework publicly available to the .NET community providing these kind of features. To demonstrate the capabilities of our framework, we also present a few client applications that take advantage of its features, such as a Big Data query optimization analysis to automatically detect unused columns and dependencies between input and output tables of user-defined operators written in a .NET-based programming language like C#.Fil: Zoppi, Edgardo Julio. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina
Improving taint analysis specificacions for javascript with big code
No full textEn la actualidad, las técnicas de análisis estático de código son una herramienta muy usada para detectar, de manera temprana, vulnerabilidades de seguridad durante etapas tempranas en el proceso de desarrollo. Taint analysis es un tipo particular de análisis, con prestaciones que lo caracterizan como un gran candidato para detectar fallas muy comunes en aplicaciones web, como son los ataques de inyección. Si bien las técnicas para llevar a cabo este tipo de análisis están ampliamente estudiadas, el mismo depende de una serie de especificaciones que indican qué elementos de un programa podrían estar involucrados en una vulnerabilidad. En esta tesis se presenta una técnica de inferencia de especificaciones de taint analysis, para el lenguaje JavaScript. La implementación de la misma surge de combinar un método ya existente basado en aprendizaje automático, con el motor de análisis estático CodeQL. La técnica presentada parte un grafo que modela la propagación de datos a lo largo de un programa, y construye un modelo de optimización lineal que resuelve el problema de inferencia de manera escalable. Las especificaciones producidas se expresan en una representación que permite generalizar un fragmento de código, para as ́ı poder reconocer casos similares en otros programas. Además, se presenta una nueva metodología de evaluación que no requiere supervisión alguna, a fin de cuantificar el potencial de la técnica para inferir nuevas especificaciones. Mediante esta metodología, se evalúa el procedimiento presentado en el trabajo, sobre un conjunto de alrededor de setecientos programas afectados por cuatro clases diferentes de vulnerabilidades de seguridad, alcanzando valores de recall cercanos al 80 %.Nowadays, static code analysis techniques are widely used tools for detecting security vulnerabilities early in the development stage. Taint analysis is a specific type of static code analysis commonly used to detect security-related problems in web applications, such as injection attacks. While the techniques for conducting taint analysis are well-studied, they depend on a set of specifications that indicate which program elements could be involved in a vulnerability. This thesis presents a technique, Jeldon, for inferring the specifications required for taint analysis in JavaScript. The implementation combines an existing machine learningbased approach with the static analysis engine CodeQL. Our approach starts with a graph that models data propagation throughout a program, then, it constructs a linear optimization model which is capable of solving the inference problem required to build the specifications in a scalable manner. The produced specifications are expressed in a representation that allows the generalization of a fragment of code, enabling the analyzer to recognize similar patterns in other programs. Additionally, we present a new methodology for quantitatively evaluating the Jeldon technique. This new methodology allows us to measure how well it performs inferring new specifications, without requiring any supervision. Using this methodology, we evaluated Jeldon on approximately 700 programs affected by four different security vulnerability kinds, achieving a recall of around 80 %.Fil: Balbi, Pablo Luis. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina
Static analysis of .NET programs.
Full text linkEn esta tesis presentamos el diseño e implementación de una amplia gama de análisis estáticos para la plataforma .NET, con foco en la escalabilidad. Nos concentramos en .NET dada su gran popularidad en la industria y el amplio conjunto de características que provee, pertenecientes a los paradigmas orientado a objetos y funcional, incluyendo programación concurrente y la manipulación de bajo nivel de punteros. La combinación de todas estas características hacen del análisis estático un desafío. Por un lado, presentamos un framework de análisis estático distribuido de programa completo, diseñado para escalar con el tamaño de la entrada. Nuestro enfoque está basado en el modelo de programación con actores para ser ejecutado en la nube. Nuestra decisión de utilizar una red de computadoras en la nube provee un grado de elasticidad para recursos de CPU, memoria y almacenamiento. Para demostrar el potencial de nuestra técnica, mostramos cómo puede ser implementado un análisis de call graph típico en una configuración distribuida. Además, extendemos nuestro análisis para soportar actualizaciones incrementales del código fuente y mostramos cómo los resultados computados previamente pueden ser actualizados sin tener que volver a calcularlos de cero. Por otro lado, presentamos un framework de análisis estático de programas y herramientas específicamente diseñado para la plataforma .NET. Este framework provee muchas funcionalidades, incluyendo algunas representaciones intermedias como el código de tres direcciones, adecuado para la implementación de un análisis estático, así como también provee una amplia gama de análisis y transformaciones como son la inferencia de tipos, los análisis de control-flow y data-flow, y la construcción de call graph y points-to graph, entre otros. No sabemos de ningún otro framework de análisis estático de código públicamente disponible para la comunidad .NET que provea este tipo de funcionalidades. Para demostrar las capacidades de nuestro framework, presentamos también algunas aplicaciones cliente que aprovechan sus funcionalidades, como un análisis de optimización de consultas Big Data para detectar automáticamente columnas no utilizadas y dependencias entre tablas de entrada y salida de operadores definidos por el usuario desarrollados en algún lenguaje de la plataforma .NET como C#.In this thesis we present the design and implementation of a wide range of static analyses for the .NET platform, with focus in scalability. We target .NET given its popularity in the industry and the rich set of features it provides, ranging from object-oriented to functional paradigms, including concurrent programming and low-level pointer manipulation. The combination of all these features make static analysis very challenging. On the one hand, we present a distributed, whole-program static analysis framework that is designed to scale with the size of the input. Our approach is based on the actor programming model and is deployed in the cloud. Our reliance on a cloud cluster provides a degree of elasticity for CPU, memory and storage resources. To demonstrate the potential of our technique, we show how a typical call graph analysis can be implemented in a distributed setting. In addition, we extend our analysis to support incremental source code updates and show how the previously computed results can be updated without having to recompute them from scratch. On the other hand, we present a static program analysis framework and tools specifically designed for the .NET platform. It provides many features, including a few intermediate code representations such as a three-address code suitable for implementing a static analysis on top of it, and a rich set of analyses and transformations such as type inference, control-flow and data-flow analyses, and call graph and points-to graph construction, among others. We don’t know of any other static analysis framework publicly available to the .NET community providing these kind of features. To demonstrate the capabilities of our framework, we also present a few client applications that take advantage of its features, such as a Big Data query optimization analysis to automatically detect unused columns and dependencies between input and output tables of user-defined operators written in a .NET-based programming language like C#.Fil: Zoppi, Edgardo Julio. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina
- …
