Métodos para el análisis de programas probabilistas y no-deterministas utilizando probadores de teoremas. Methods for the analysis of probabilistic and nondeterministic programs using theorem provers.

La verificación y el análisis de programas con características probabilistas es una tarea necesaria del quehacer científico y tecnológico actual. El éxito y su posterior masificación de las implementaciones de protocolos de comunicación a nivel hardware y soluciones probabilistas a problemas distribuidos hacen más que interesante el uso de agentes estocásticos como elementos de programación. En muchos de estos casos el uso de agentes aleatorios produce soluciones mejores y más eficientes; en otros proveen soluciones donde es imposible encontrarlas por métodos tradicionales. Estos algoritmos se encuentran generalmente embebidos en múltiples mecanismos de hardware, por lo que un error en los mismos puede llegar a producir una multiplicación no deseada de sus efectos nocivos.Actualmente el mayor esfuerzo en el análisis de programas probabilísticos se lleva a cabo en el estudio y desarrollo de herramientas denominadas chequeadores de modelos probabilísticos. Las mismas, dado un modelo finito del sistema estocástico, obtienen de forma automática varias medidas de performance del mismo. Aunque esto puede ser bastante útil a la hora de verificar programas, para sistemas de uso general se hace necesario poder chequear especificaciones más completas que hacen a la corrección del algoritmo. Incluso sería interesante poder obtener automáticamente las propiedades del sistema, en forma de invariantes y contraejemplos.En este proyecto se pretende abordar el problema de análisis estático de programas probabilísticos mediante el uso de herramientas deductivas como probadores de teoremas y SMT solvers. Las mismas han mostrado su madurez y eficacia en atacar problemas de la programación tradicional. Con el fin de no perder automaticidad en los métodos, trabajaremos dentro del marco de "Interpretación Abstracta" el cual nos brinda un delineamiento para nuestro desarrollo teórico. Al mismo tiempo pondremos en práctica estos fundamentos mediante implementaciones concretas que utilicen aquellas herramientas.

Holonomia, geometría homogénea, dinámica topológica y rango de variedades riemannianas

Se estudiará la geometría de subvariedades haciendo hincapié en los grupos de holonomia de la conexión normal, herramienta que ha sido muy útil para atacar diversos problemas clásicos. Se estudiarán los siguientes problemas concretos: a) Resolver la conjetura de que toda subvariedad homogénea irreducible y substancial de la esfera cuyo grupo de holonomia normal no actúa transitivamente en la esfera es una órbita de la representación isotrópica de un espacio simétrico simple. b) ¿Existe alguna relación entre la noción de rango para espacios de curvatura no positiva y la noción de rango de una subvariedad? Respecto al rango de las variedades riemannianas se intenta probar un teorema general de descomposición para variedades riemannianas tal que toda geodésica esté contenida en un flat compacto. (...) Intentará generalizar los siguientes teoremas, válidos para flujos, a extensiones entre flujos, usando el concepto de semigrupo envolvente de una extensión. 1. X métrico y los elementos de E(X) son continuos, entonces E(X) es métrico. 2. Si se agrega la hipótesis de minimal, entonces X es equicontinuo. 3. X minimal, los elementos de E(X) de continuos y T contable entonces es equicontinuo. 4. X minimal y E(X) conmutativo entonces X es equicontinuo. 5. X distal y los elementos de E(X) son continuos, entonces X es equicontinuo.

Aplicaciones de la teoría de PDE a la relatividad general

Este plan de trabajo contempla diversas aplicaciones de la teoría de las Ecuaciones en Derivadas Parciales en el contexto de la Relatividad General. (...) Estas aplicaciones tiene como una de las intenciones últimas la de ser empleadas en simulaciones numéricas. Entre ellas destacamos las siguientes: * Fluidos viscosos relativistas y sus límites parabólicos. * Modelado numérico de las ecuaciones del primer punto. * Existencia global de sistemas disipativos. * Teoremas no-hair cosmológicos. * Límite Newtoniano de la relatividad general, resultados rigurosos. * Condiciones de contorno para las ecuaciones de Einstein.

Representaciones de grupos y álgebras de Lie

Este proyecto cuenta con 7 subproyectos.Subproyecto: Restricciones de representaciones de cuadrado integrable.Se continuará trabajando en el problema de restringir representaciones de cuadrado integrable en un grupo de Lie a un subgrupo semisimple o la factor unipotente de un subgrupo parabólico. En particular, se continuará analizando el caso de restringir desde el grupo SO(2n,1) al subgrupo SO(2) x SO(2n-2,1) y al factor unipotente del parabólico minimal de un grupo de Lie clásico de rango uno. Subproyecto: Representación metapléctica y grupos de Heisenberg generalizados. Se estudia la restricción de la representación metapléctica a subgrupos del grupo metapléctico. Subproyecto: Álgebras de tipo H. Se estudiarán estructuras de biálgebra en las álgebras de tipo H, álgebras de Lie nilpotentes de dos etapas. Se continuará con el estudio de cuantizaciones de álgebras de tipo H. Se estudiarán propiedades geométricas de las funciones theta generalizadas que surgen de álgebras de tipo H. Subproyecto: Módulos de peso máximo. Se intenta dar una respuesta al problema de clasificación de módulos quasifinitos de peso máximo sobre ciertas álgebras de dimensión infinita. Subproyecto: Cuantización de las álgebras de tipo H. Se tratará de cuantizar las álgebras de tipo H, álgebras de Lie nilpotentes de dos etapas. Se trabajará con una definición más general de las álgebras de Heisenberg, tratando de encontrar teoremas tipo Stone-Von Neumann y generalizaciones de las funciones theta. Subproyecto: Continuación analítica de integrales de coeficientes matriciales. Se analiza la existencia de continuación holomorfa de la integral a lo largo de un grupo semisimple real de las potencias complejas de un coeficiente matricial de una representación irreducible admisible. Subproyecto: Cálculo explícito de soluciones fundamentales de operadores invariantes. Se analizan condiciones en el polinomio que define un operador diferencial k-invariante para que resulte hipoellítico. Se trata en particular el caso del grupo SO(n,1). Subproyecto 7: Generadores de Goldie. Se trata de encontrar algoritmos para el cálculo de generadores de Goldie.

Algebras de Lie de tipo H

Es mi intención centrar mis investigaciones en los próximos años en las álgebras de Lie tipo H. Es nuestro objetivo encontrar nuevas familias de álgebras regulares no de tipo H y verificar la existencia o no de irreducibles cumpliendo de estas propiedades. En particular es interesante plantear su cuantización, es decir encontrar estructuras de álgebras de Hopf que sean deformaciones del álgebra envolvente correspondiente al álgebra de Lie en estudio. En particular estudiaremos si existen cuantizaciones quasitriangulares lo que nos llevaría soluciones de la ecuación de Yang-Baxter cuántica. Hasta ahora hemos logrado la cuantización en ciertos casos particulares. Para comprender cómo deben ser hechas las cuantizaciones en forma más general es necesario realizar un estudio sistemático de las estructuras de la biálgebra de las álgebras de Lie de tipo H. En particular se tratarán de detectar estructuras de biálgebra quasitriangulares y por consiguientes soluciones de la ecuación de Yang-Baxter clásica. Es un resultado conocido que las funciones de theta se pueden expresar como coeficiente matricial de la representación de Stone-Von Neumann. De los teoremas de Stone-Von Neumann para álgebras de tipo H surgen entonces funciones que serían una generalización de las funciones theta; es nuestro objetivo encontrar propiedades de estas funciones que puedan ser de interés.

Filososofía y Ciencia Computacional: Aspectos epistemológicos, ontológicos y metodológicos. Philosophy and Computing Sciencs: Epistemological, Ontological and Methodological Aspects.

Uno de los temas centrales del proyecto concierne la naturaleza de la ciencia de la computación. La reciente aparición de esta disciplina sumada a su origen híbrido como ciencia formal y disciplina tecnológica hace que su caracterización aún no esté completa y menos aún acordada entre los científicos del área. En el trabajo Three paradigms of Computer Science de A. Eden, se presentan tres posiciones admitidamente exageradas acerca de como entender tanto el objeto de estudio (ontología) como los métodos de trabajo (metodología) y la estructura de la teoría y las justificaciones del conocimiento informático (epistemología): La llamada racionalista, la cual se basa en la idea de que los programas son fórmulas lógicas y que la forma de trabajo es deductiva, la tecnocrática que presenta a la ciencia computacional como una disciplina ingenieril y la ahi llamada científica, la cual asimilaría a la computación a las ciencias empíricas. Algunos de los problemas de ciencia de la computación están relacionados con cuestiones de filosofía de la matemática, en particular la relación entre las entidades abstractas y el mundo. Sin embargo, el carácter prescriptivo de los axiomas y teoremas de las teorías de la programación puede permitir interpretaciones alternativas y cuestionaría fuertemente la posibilidad de pensar a la ciencia de la computación como una ciencia empírica, al menos en el sentido tradicional. Por otro lado, es posible que el tipo de análisis aplicado a las ciencias de la computación propuesto en este proyecto aporte nuevas ideas para pensar problemas de filosofía de la matemática. Un ejemplo de estos posibles aportes puede verse en el trabajo de Arkoudas Computers, Justi?cation, and Mathematical Knowledge el cual echa nueva luz al problema del significado de las demostraciones matemáticas.Los objetivos del proyecto son: Caracterizar el campo de las ciencias de la computación.Evaluar los fundamentos ontológicos, epistemológicos y metodológicos de la ciencia de la computación actual.Analizar las relaciones entre las diferentes perspectivas heurísticas y epistémicas y las practicas de la programación.

Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.