Descripción: Cuando se consideran las maneras de producir programas, la técnica principal queviene a la mente de cada uno de nosotros es la de escribir el programa a mano. Aunqueexisten técnicas de derivación y herramientas para producir programas automáticamente,su aplicación está usualmente restringida a cierta clase de problemas, o ciertos dominios (como los generadores de parsers, o las interfaces visuales). En los casos donde talestécnicas se pueden aplicar, la productividad y la confiabilidad se ven ampliamente incrementadas. Por esa razón, nos interesamos en la producción automática de programasen un marco general. La especialización de programas es una manera particular de producir programasautomáticamente. En ella se utiliza un programa fuente general dado para generardiversas versiones particulares, especializadas, del mismo, cada una resolviendo una instanciaparticular del problema original. La técnica más conocida y más ampliamenteestudiada de especialización de programas es llamada evaluación parcial; se la ha utilizadocon éxito en varias áreas de aplicación diferentes. Sin embargo, la evaluaciónparcial tiene problemas cuando se considera la producción automática de programas contipos. La especialización de tipos es una forma de especialización de programas que puedeproducir automáticamente programas con tipos a partir de uno fuente. Comprendediversas técnicas muy poderosas, tales como especialización polivariante, especializaciónde constructores, conversión de clausuras; es la primera de las variantes de especializaciónde programas que puede generar tipos arbitrarios a partir de un único programa fuente. Creemos que la especialización de tipos puede ser la base sobre la que desarrollar unmarco de producción automática de programas. En esta tesis consideramos la especialización de programas, extendiéndola para producirprogramas polimórficos. Ilustramos eso considerando un intérprete para un lambdacálculo con tipos a la Hindley-Milner, y especializándolo con cualquier programa objetopara producir un programa residual que sea esencialmente igual que el original. En labúsqueda de la generación de polimorfismo, extendemos la especialización de tipos paraque pueda expresar la especialización de programas con información estática incompleta,y probamos que para cada término podemos inferir una especialización particular quepuede ser usada para reconstruir cada uno de las otras especializaciones de tal término. Llamamos especialización de tipos principal a tal técnica, debido a la analogía de estapropiedad con la noción de tipos principales. Nuestra presentación clarifica muchos delos problemas existentes en la especialización de tipos, lo cual puede ser usado como unaguía en la búsqueda de soluciones para ellos. La presentación se divide en cuatro partes. En la primera Parte, presentamos la Especialización de Tipos en su forma original, junto con material complementario. Enla Parte II desarrollamos la presentación de la Especialización de Tipos Principal, explicandotodos los detalles técnicos, dando varios ejemplos, y presentando nuestra implementación del prototipo. En la Parte III describimos las posibilidades de la formulaciónnueva, proveyendo una extensión de la Especialización de Tipos para generar programaspolimórficos. Finalmente, la última parte describe trabajos relacionados, trabajosfuturos, y concluye. Este trabajo es el resultado de siete a˜nos de investigación, realizados durante misestudios de doctorado.

Descripción: Las herramientas de análisis estático de código han mostrado un progresosignificativo en la última década. Una de las formulaciones del problema aresolver es el de descubrir si una propiedad es satisfecha necesariamente porun determinado sistema bajo análisis o si, por el contrario, existen ejecuciones de dicho sistema que violan la propiedad deseada. Dicha enunciación del problema es conocida como Software Model Checking y el mismo es indecidible en el caso caso general. Habitualmente las herramientas de Software Model Checking buscan llegara estar en condiciones de producir un resultado afirmativo, confirmando quela propiedad es satisfecha, o negativo, que habitualmente incluye un contraejemplo que viola la propiedad en cuestión. Sin embargo, en muchos casos, las herramientas se ven obligadas a producir un tercer resultado que indica que no se pudo demostrar la propiedad pero tampoco generar un contraejemplo. Además de los límites teóricos mencionados, en la práctica el problema resulta intratable para una gran cantidad de instancias de relevancia debido a que insume una elevada cantidad de recursos y de tiempo, incluso para casos en los que se alcanzaría finalmente una solución. En estos casos la gran mayoría de las herramientas indican al usuarioúnicamente que el intento de verificación no alcanzó un resultado concluyente, sin ninguna aclaración adicional. Este trabajo se centra en proveer al usuario información adicional en dichos intentos de verificación. Con ese objetivo en mente, proponemos distintas formas de presentar e interpretar la información que se puede extraer en esos casos, teniendo en cuenta distintos posibles grados de familiaridad con las técnicas de verificación subyacente por parte del usuario. En particular, nos centramos en una amplia familia de técnicas de verificación y presentamos varias vistas del progreso realizado por la herramienta previo a interrumpir el intento de verificación, acompañadas de su correspondiente caracterización formal. Adicionalmente, adaptamos la noción de cobertura, más frecuentemente utilizada en testing, a la familia de técnicas analizada. En ambos casos brindamos algoritmos que generan automáticamentetanto las vistas propuestas como sub-aproximaciones de la métrica de cobertura. Las técnicas propuestas son evaluadas sobre instancias de referencias ampliamente utilizadas tanto para determinar la practicalidad en cuanto al tiempo de ejecución requerido como para analizar la interpretabilidad de los resultados generados. La experimentación realizada confirma que es factible extraer informacióna partir de resultados inconcluyentes e interpretar dichos resultados revelando información no trivial.

Descripción: Sea k un cuerpo perfecto infinito, k[xl, . . . ,xn] el anillo de polinomios en n variables y F ϵ k[x1,. . . ,xn]MxM una matriz polinomial de una proyección. Si sus entradas estándadas por un straight line program de tamaño L y sus grados acotados por D, mostramosque existe un algoritmo bien paralelizable que computa una base del núcleo y de la imagende F en tiempo (nL)°(¹)(MD)°(ⁿ). Este resultado nos permite obtener, haciendo uso de la teoría de trazas, un algoritmosimplemente exponencial que computa una base para un anillo intersección completa enposición de Noether. Además, como una consecuencia de nuestras técnicas podemos mostrar un algoritmo simplementeexponencial que decide si un k[x1, . . . ,xn]-módulo finito dado por una matrizde presentación es libre y, en ese caso, exhibir una base.

Descripción: En 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#.

Descripción: En esta tesis, investigamos algunos aspectos de aleatoriedad y trivialidad definidos por la teoría de largo de programa. Primero abordamos la aleatoriedad y la absoluta normalidad de números reales. Ambos conjuntos de reales tienen medida de Lebesgue 1 y son nociones que implican varias propiedades de estocasticidad. A pesar de esto, no ha sido fácil dar ejemplos concretos en estas clases. Probamos que existen números absolutamente normales que son computables y damos dos algoritmos para construirlos. El primero está basado en una reformulación computable de un resultado de Sierpinski de 1916. El segundo es parte de nuestra reconstrucción de un manuscrito inédito de Turing sobre números normales. En cuanto a ejemplos de aleatoriedad, generalizamos la probabilidad de detención de Chaitin y analizamos la probabilidad de que una máquina universal se detenga y devuelva un resultado en un conjunto dado X. Estudiamos la relación entre las propiedades de X provenientes de la teoría de la computabilidad y las propiedades de aleatoriedad de la probabilidad inducida. El segundo aspecto de aleatoriedad que tratamos es el estudio de una variante de la complejidad clásica de largo de programa que no involucra oráculos, y nos preguntamos si esta noción conduce a una definición más estricta de aleatoriedad. Definimos nuestra función de complejidad en base a máquinas de Turing monótonas que realizan cómputos infinitos. Investigamos algunas propiedades de esta función y consideramos las definiciones inducidas de aleatoriedad y trivialidad. Con esta última noción caracterizamos a los reales computables. El último aspecto se vincula con la anti-aleatoriedad y la posibilidad de caracterizar a los reales llamados K-triviales con nociones que no involucren directamente a la complejidad de largo de programa libre de prefijos. Proponemos e investigamos dos nociones de lowness que tienen sus raíces puramente en la teoría de la computabilidad, reforzando otras ya existentes en la literatura. Relacionamos la complejidad de largo de programa plana C y libre de prefijos K con estas nociones, considerando variaciones de K-trivialidad y C-trivialidad. Concluimos con una lista de las principales preguntas que quedaron abiertas.