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.

Modelización numérica de problemas geológico-geotécnicos

Los proyectos geotécnicos, ya sean civiles, mineros, de desarrollo urbano, etcétera, en la medida que implican afectaciones del medio físico, necesitan disponer de un modelo geológico y geomecánico con fines de una concepción racional con dimensionamiento adecuado y seguro. En este sentido la línea de desarrollo e investigaciones ya comenzada en el marco interdisciplinario (geotécnico, matemático y computacional) tiende a instrumentar modelizaciones geológico-geotécnicas que de acuerdo a la experiencia de los directores resultan mayormente aplicables a la solución de problemas en el campo de la geomecánica. De este modo las actividades previstas en el presente plan de trabajo son las siguientes: 1. Cuantificación estocástica de la geometría de macizos rocosos. Se aplicarán nuevos aportes a la modelización estructural ya realizada, tendiente al abordaje estocástico de la bloquimetría de los macizos rocosos. 2. Estabilidad de Taludes por equilibrio límite, evaluación probabilística del factor de seguridad. Se investigarán aproximaciones probabilística de este tipo de falla, utilizando variables randómicas de input. 3. Modelo predictivo para la deformabilidad de macizos rocosos. Los estudios en este aspecto tratarán el desarrollo de un sistema analítico de evaluación, con base estadística y experimental orientado a la evaluación de la deformabilidad de los macizos rocosos fracturados. 4. Modelización estructural aplicada a la determinación de la permeabilidad de macizos rocosos. Se estudiarán relaciones entre el tensor de permeabilidad de los macizos rocosos y las condiciones de fracturamiento de los mismos.

Aplicación de la Resonancia Magnética Nuclear al estudio de sólidos moleculares

La Resonancia Magnética Nuclear (RMN) y la Resonancia Cuadrupolar Nuclear (RCN) son técnicas sumamente útiles para el estudio microscópico de diversas propiedades estructurales y dinámicas en sólidos. Nuestro grupo de investigación posee una amplia experiencia en la aplicación de ambas técnicas para la caracterización de cristales moleculares. Sin embargo, la limitada infraestructura existente en el área de la RMN ha hecho que esta importante técnica no fuera utilizada en toda su potencialidad. Objetivos generales y específicos El Objetivo de este plan de trabajo es optimizar la infraestructura experimental con el propósito de utilizar esta técnica en los diversos proyectos de la Física del Sólido que se desarrolla en nuestro grupo de trabajo. En particular, se aplicará el estudio de compuestos pertenecientes a la familia de los bifenilos clorados analizando cómo afectan las interacciones intermoleculares a la conformación de la molécula llegando a originar, en algunos casos, la aparición de transiciones de fase a estructuras desordenadas o parcialmente desordenadas evidenciadas en cambios estructurales y dinámicos de la molécula. También se planifica estudiar cómo perturbaciones a las interacciones intermoleculares modifican las características de las transiciones a estas estructuras parcialmente desordenadas. Se espera desarrollar una infraestructura experimental que permita el desarrollo de nuevas líneas de investigación, muchas de las cuales se realizan de manera precaria con el instrumental existente. (...) El objetivo de este proyecto es desarrollar la infraestructura experimental del grupo de investigación de manera tal de aplicar la técnica de RMN al estudio de las propiedades estructurales y dinámicas de los sólidos moleculares que presentan un cierto grado de desorden estructural. Es por ello que se planean como objetivos específicos: a) Puesta en funcionamiento del espectrómetro de RMN donado por la Facultad de Farmacia y Bioquímica de la Universidad de Buenos Aires. (...) b) Aplicación de la técnica de RMN para el estudio de cristales moleculares pertenecientes a la familia de los bifenilos clorados.

Resonancia Magnética Nuclear en aleaciones moleculares y sistemas heterogéneos

La Resonancia Cuadrupolar Nuclear ha tratado desde siempre de resolver uno de los problemas de la Física del Sólido que es el estudio de cristales impuros, en particular, la naturaleza y concentración de moléculas de impurezas en cristales moleculares. Estos estudios han presentado problemas relacionados con los diagramas de estado de las soluciones sólidas y las condiciones asociadas al enfriamiento ya que se encontraban una variedad de soluciones con concentraciones diferentes a las del "melt". Las aleaciones de compuestos moleculares A(x)B(1-x) son materiales cuya originalidad y riqueza están en que variando la composición, la temperatura de fusión puede ser ajustada a condiciones óptimas de trabajo. Estas propiedades los convierte en tecnológicamente atractivos, particularmente como almacenadores de energía y protectores térmicos. Para comprender el proceso de formación de una aleación molecular es de fundamental importancia el conocimiento de las estructuras, las diferentes fases termodinámicas y la estabilidad de las mismas. (...) Los objetivos más inmediatos del estudio de las aleaciones por RCN son: a) Determinar la naturaleza física de las interacciones que se manifiestan en los espectros de RCN. b) Determinar las leyes estadísticas que describen la distribución de moléculas de "impurezas sustitucionales" en el cristal de la aleación. c) Determinar la influencia de factores de simetría en el espectro de RCN de las aleaciones. Por otra parte, dado lo laborioso y complejo de la determinación de los diagramas de fase y estabilidad de las mismas, se utilizan los métodos de la Mecánica Estadística para calcular los diagramas de fase de las aleaciones moleculares. Las simulaciones Montecarlo de hamiltonianos tipo Ising utilizadas para modelar estas aleaciones binarias permitirán además comprobar la validez de los potenciales transferibles átomo-átomo en los bencenos sustituidos al utilizarlos éstos para calcular las constantes de acoplamiento Jij.

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.

Fluctuaciones de orden local en sistemas moleculares

Existe actualmente un interés muy difundido por los fluidos anisotrópicos (cristales líquidos, polímeros) debido a la gran cantidad de aplicaciones que se pueden realizar con ellos (por ejemplo en la fabricación de displays, en medicina, biología, etc.). Su estudio también planea interesantes problemas desde un punto de vista de la física fundamental. Sin embargo, a pesar de esto es muy poco lo que se conoce acerca de la dinámica molecular, y el problema está abierto. Las técnicas más apropiadas en este campo son el estudio de las propiedades dieléctricas y la RMN (relajación spin-red). En esta última, hay una gran actividad en el campo experimental con el desarrollo de numerosas técnicas nuevas. Sin embargo, desde el punto de vista de la teoría de la relajación se continúa utilizando aproximaciones semiclásicas. Entonces, es necesario revisar las hipótesis fundamentales de la teoría de la RMN con el fin de extender su campo de aplicación a problemas complejos como los que plantean los fluidos anistrópicos. El propósito general de esta línea de trabajo es el de extender la teoría semiclásica de relajación nuclear en RMN para incluir la naturaleza cuántica del fenómeno. Al cabo de esta investigación se espera poder describir la relajación del orden dipolar en mesofaces ordenadas como los cristales líquidos, ferrofluídos, etc. (...) Al cabo de este período se espera avanzar en las siguientes tareas: 1. Contar con una ecuación maestra para la matriz densidad de spin lo suficientemente general para incluir los efectos mencionados, pero que a la vez permita la comparación con los resultados experimentales. Dejando de lado las suposiciones clásicas de alta temperatura y orden débil, y en el marco de la suposición de temperatura de spin, se estudiará una expansión de la ecuación maestra en inversas de las temperaturas de la red y de spin. Conservando términos de orden mayor que lineal (aproximación clásica) e introduciendo las interacciones spin-spin durante el tiempo de correlación de la red (memoria microscópica) se analizará la dependencia con la frecuencia de Larmor de T1D y T1Z. Las interacciones spin-spin se introducirán mediante un método perturbativo de operadores. 2. Comprender la razón física de la diferencia de comportamiento con la frecuencia de Larmor de los parámetros T1D y T1Z. 3. Generalizar el análisis para aplicarlo al tiempo de relajación spin-red en el sistema rotante T1r.

Modelos Mixtos-Aditivos Generalizados para el Estudio de Fenómenos Biológicos y Sociales Descriptos por Datos Agregados y/o Longitudinales. Generalized Mixed Additive Models for the Study of Biological and Social Phenomenons from Longitudinal and/or Aggregated Data.

Este proyecto propone extender y generalizar los procesos de estimación e inferencia de modelos aditivos generalizados multivariados para variables aleatorias no gaussianas, que describen comportamientos de fenómenos biológicos y sociales y cuyas representaciones originan series longitudinales y datos agregados (clusters). Se genera teniendo como objeto para las aplicaciones inmediatas, el desarrollo de metodología de modelación para la comprensión de procesos biológicos, ambientales y sociales de las áreas de Salud y las Ciencias Sociales, la condicionan la presencia de fenómenos específicos, como el de las enfermedades.Es así que el plan que se propone intenta estrechar la relación entre la Matemática Aplicada, desde un enfoque bajo incertidumbre y las Ciencias Biológicas y Sociales, en general, generando nuevas herramientas para poder analizar y explicar muchos problemas sobre los cuales tienen cada vez mas información experimental y/o observacional.Se propone, en forma secuencial, comenzando por variables aleatorias discretas (Yi, con función de varianza menor que una potencia par del valor esperado E(Y)) generar una clase unificada de modelos aditivos (paramétricos y no paramétricos) generalizados, la cual contenga como casos particulares a los modelos lineales generalizados, no lineales generalizados, los aditivos generalizados, los de media marginales generalizados (enfoques GEE1 -Liang y Zeger, 1986- y GEE2 -Zhao y Prentice, 1990; Zeger y Qaqish, 1992; Yan y Fine, 2004), iniciando una conexión con los modelos lineales mixtos generalizados para variables latentes (GLLAMM, Skrondal y Rabe-Hesketh, 2004), partiendo de estructuras de datos correlacionados. Esto permitirá definir distribuciones condicionales de las respuestas, dadas las covariables y las variables latentes y estimar ecuaciones estructurales para las VL, incluyendo regresiones de VL sobre las covariables y regresiones de VL sobre otras VL y modelos específicos para considerar jerarquías de variación ya reconocidas. Cómo definir modelos que consideren estructuras espaciales o temporales, de manera tal que permitan la presencia de factores jerárquicos, fijos o aleatorios, medidos con error como es el caso de las situaciones que se presentan en las Ciencias Sociales y en Epidemiología, es un desafío a nivel estadístico. Se proyecta esa forma secuencial para la construcción de metodología tanto de estimación como de inferencia, comenzando con variables aleatorias Poisson y Bernoulli, incluyendo los existentes MLG, hasta los actuales modelos generalizados jerárquicos, conextando con los GLLAMM, partiendo de estructuras de datos correlacionados. Esta familia de modelos se generará para estructuras de variables/vectores, covariables y componentes aleatorios jerárquicos que describan fenómenos de las Ciencias Sociales y la Epidemiología.

Analisis De Mercados De Energía Eléctrica Competitivos Con Participación De Energía Eólica. Competitive Electricity Markets Analisis with Wind Power Generation.

La utilización de energía eólica es un hecho cada vez más común en nuestro mundo como respuesta a mitigar el creciente aumento de demanda de energía, los aumentos constantes de precio, la escasez de combustibles fósiles y los impactos del cambio climático, los que son cada día más evidentes.Consecuentemente, el interés por la participación de esta nueva forma de generación de energía en sistema eléctrico de potencia ha aumentado considerablemente en los últimos años. La incorporación de generación de origen eólico en el sistema eléctrico de potencia requiere de un análisis detallado del sistema eléctrico en su conjunto, considerando la interacción entre parques y unidades de generación eólica, plantas de generación convencional y el sistema eléctrico de potencia. La integración de generación de origen renovable en el sistema eléctrico de potencia convencional presenta nuevos desafíos los que pueden ser atribuidos a características propias de este tipo de generación, por ejemplo la fluctuación de energía debido a la naturaleza variable del viento, la naturaleza distribuida de la generación eólica y las características constructivas y método de conexión de los distintos modelos de turbinas eólicas al sistema.La finalidad de este proyecto de investigación consiste en investigar el impacto sobre un mercado de sistema eléctrico competitivo causado por el agregado de generación de origen eolico. Como punto de partida se pretende realizar modelos de plantas de generacion eolica para luego incorporarlos a los modelos de sistemas eléctricos y realizar estudios de de despacho económico, flujo de cargas, análisis transitorio y estudios dinámicos del sistema.

Dinámica Cuántica de Sistemas Complejos: Fundamentos y Aplicaciones. Quantum Dynamics in Complex Systems: Fundamentals and Aplications.

El procedimiento de revertir la dinámica colectiva (diablillo de Loschmidt apresurado) mediante un pulso de radio frecuencia, permite generar un Eco de Loschmidt, es decir la refocalización de una excitación localizada. Alternativamente, en acústica es posible implementar un Espejo de Reversión Temporal, que consiste en la progresiva inyección de una débil excitación ultrasónica en la periferia de un sistema, para construir una excitación que se propaga "hacia atrás". Así, podemos afirmar que es posible revertir y controlar la dinámica. Sin embargo, aún no se posee una comprensión detallada de los mecanismos que gobiernan estos procedimientos. Este proyecto busca responder las preguntas que posibilitan esta comprensión.

Estructura, representaciones y cohomología de álgebras de Lie nilpotents. Structure, represntations and cohomology of nilpotent Lie algebras.

El objetivo de este proyecto es obtener resultados de calidad en el área de las representaciones y cohomología de álgebras de Lie complejas nilpotentes de dimensión finita. Los objetivos específicos son (1) Demostrar que la familia de nilradicales parabólicos de las subálgebras de Lie semisimples satisfacen la conjetura del rango toral. (2) Calcular explícitamente la cohomología, aunque sea en grados bajos, de las álgebras de Lie 3-pasos nilpotentes libres y las álgebras $\mathfrak{gl}(2,A_{k})$ donde $A_{k}$ es el álgebra de quiver truncada en $k$ asociada a un quiver cíclico de $k$ flechas (y $k$ vértices). (3) Determinar explícitamente qué diagramas de Young aparecen en la cohomología, calculada por Kostant, de los nilradicales parabólicos de las subálgebras de Lie semisimples. (4) Mejorar las actuales cotas para las representaciones fieles de dimensión mínima de álgebras de Lie 3-pasos nilpotentes.

Optimización en el cómputos de algoritmos de cuadratura para funciones especiales. Optimization of quadrature algorithms for special functions.

En nuestro proyecto anterior aproximamos el cálculo de una integral definida con integrandos de grandes variaciones funcionales. Nuestra aproximación paraleliza el algoritmo de cómputo de un método adaptivo de cuadratura, basado en reglas de Newton-Cote. Los primeros resultados obtenidos fueron comunicados en distintos congresos nacionales e internacionales; ellos nos permintieron comenzar con una tipificación de las reglas de cuadratura existentes y una clasificación de algunas funciones utilizadas como funciones de prueba. Estas tareas de clasificación y tipificación no las hemos finalizado, por lo que pretendemos darle continuidad a fin de poder informar sobre la conveniencia o no de utilizar nuestra técnica. Para llevar adelante esta tarea se buscará una base de funciones de prueba y se ampliará el espectro de reglas de cuadraturas a utilizar. Además, nos proponemos re-estructurar el cálculo de algunas rutinas que intervienen en el cómputo de la mínima energía de una molécula. Este programa ya existe en su versión secuencial y está modelizado utilizando la aproximación LCAO. El mismo obtiene resultados exitosos en cuanto a precisión, comparado con otras publicaciones internacionales similares, pero requiere de un tiempo de cálculo significativamente alto. Nuestra propuesta es paralelizar el algoritmo mencionado abordándolo al menos en dos niveles: 1- decidir si conviene distribuir el cálculo de una integral entre varios procesadores o si será mejor distribuir distintas integrales entre diferentes procesadores. Debemos recordar que en los entornos de arquitecturas paralelas basadas en redes (típicamente redes de área local, LAN) el tiempo que ocupa el envío de mensajes entre los procesadores es muy significativo medido en cantidad de operaciones de cálculo que un procesador puede completar. 2- de ser necesario, paralelizar el cálculo de integrales dobles y/o triples. Para el desarrollo de nuestra propuesta se desarrollarán heurísticas para verificar y construir modelos en los casos mencionados tendientes a mejorar las rutinas de cálculo ya conocidas. A la vez que se testearán los algoritmos con casos de prueba. La metodología a utilizar es la habitual en Cálculo Numérico. Con cada propuesta se requiere: a) Implementar un algoritmo de cálculo tratando de lograr versiones superadoras de las ya existentes. b) Realizar los ejercicios de comparación con las rutinas existentes para confirmar o desechar una mejor perfomance numérica. c) Realizar estudios teóricos de error vinculados al método y a la implementación. Se conformó un equipo interdisciplinario integrado por investigadores tanto de Ciencias de la Computación como de Matemática. Metas a alcanzar Se espera obtener una caracterización de las reglas de cuadratura según su efectividad, con funciones de comportamiento oscilatorio y con decaimiento exponencial, y desarrollar implementaciones computacionales adecuadas, optimizadas y basadas en arquitecturas paralelas.

Métodos estadístico-computacionales para la caracterización de patrones de expresión de proteínas en 2D-DIGE.

El volumen de datos provenientes de experimentos basados en genómica y poteómica es grande y de estructura compleja. Solo a través de un análisis bioinformático/bioestadístico eficiente es posible identificar y caracterizar perfiles de expresión de genes y proteínas que se expresan en forma diferencial bajo distintas condiciones experimentales (CE). El objetivo principal es extender las capacidades computacionales y analíticos de los softwares disponibles de análisis de este tipo de datos, en especial para aquellos aplicables a datos de electroforésis bidimensional diferencial (2D-DIGE). En DIGE el método estadístico más usado es la prueba t de Student cuya aplicación presupone una única fuente de variación y el cumplimiento de ciertos supuestos distribucionales de los datos (como independencia y homogeneidad de varianzas), los cuales no siempre se cumplen en la práctica, pudiendo conllevar a errores en las estimaciones e inferencias de los efectos de interés. Los modelos Generalizados lineales mixtos (GLMM) permiten no solo incorporar los efectos que, se asume, afectan la variación de la respuesta sino que también modelan estructuras de covarianzas y de correlaciones más afines a las que se presentan en la realidad, liberando del supuesto de independencia y de normalidad. Estos modelos, más complejos en esencia, simplificarán el análisis debido a la modelización directa de los datos crudos sin la aplicación de transformaciones para lograr distribuciones más simétricas,produciendo también a una estimación estadísticamente más eficiente de los efectos presentes y por tanto a una detección más certera de los genes/proteínas involucrados en procesos biológicos de interés. La característica relevante de esta tecnología es que no se conoce a priori cuáles son las proteínas presentes. Estas son identificadas mediante otras técnicas más costosas una vez que se detectó un conjunto de manchas diferenciales sobre los geles 2DE. Por ende disminuir los falsos positivos es fundamental en la identificación de tales manchas ya que inducen a resultados erróneas y asociaciones biológica ficticias. Esto no solo se logrará mediante el desarrollo de técnicas de normalización que incorporen explícitamente las CE, sino también con el desarrollo de métodos que permitan salirse del supuesto de gaussianidad y evaluar otros supuestos distribucionales más adecuados para este tipo de datos. También, se desarrollarán técnicas de aprendizaje automática que mediante optimización de funciones de costo específicas nos permitan identificar el subconjunto de proteínas con mayor potencialidad diagnóstica. Este proyecto tiene un alto componente estadístico/bioinformática, pero creemos que es el campo de aplicación, es decir la genómica y la proteómica, los que más se beneficiarán con los resultados esperados. Para tal fin se utilizarán diversas bases de datos de distintos experimentos provistos por distintos centros de investigación nacionales e internacionales.

MATERIALES CON PROPIEDADES MAGNÉTICAS Y MULTIFERROICAS

Los materiales con propiedades multiferroicas, los materiales mesoporosos y óxidos mixtos con propiedades magnéticas constituyen en la actualidad temas de alto interés científico y con potencial para la búsqueda de aplicaciones tecnológicas. En este proyecto se estudiarán materiales con propiedades magnéticas y multiferroicas con potenciales aplicaciones tecnológicas. Basándonos en la amplia experiencia y reconocida trayectoria del Grupo Ciencia de Materiales en el estudio de materiales magnéticos, se desea continuar y profundizar el estudio de materiales, técnicas de producción y de caracterización recientemente incorporados al espectro de posibilidades de investigación del grupo. Los materiales serán producidos principalmente empleando las técnicas de aleado mecánico, síntesis química, electrodeposición y deposición láser pulsada. Estos materiales producidos, serán caracterizados en su morfología y por sus propiedades funcionales utilizando técnicas de caracterización disponibles en el grupo de investigación (difracción de rayos X, magnetometría de muestra vibrante(VSM), Calorimetría diferencial y balanza termogravimétrica (DSC-TGA), microscopia electrónica de barrido (SEM), Microanálisis (EMPA)) como las que se acceden a través de la Red Nacional de Magnetismo (SQUID, PPMS ). También se incluirán otras técnicas de caracterización a las cuales se accede mediante convenios específicos.

Verificación Formal de Sistemas basada Formal Software Verification based on Automated Analysisen Análisis Automático.

Identificación y caracterización del problema. Uno de los problemas más importantes asociados con la construcción de software es la corrección del mismo. En busca de proveer garantías del correcto funcionamiento del software, han surgido una variedad de técnicas de desarrollo con sólidas bases matemáticas y lógicas conocidas como métodos formales. Debido a su naturaleza, la aplicación de métodos formales requiere gran experiencia y conocimientos, sobre todo en lo concerniente a matemáticas y lógica, por lo cual su aplicación resulta costosa en la práctica. Esto ha provocado que su principal aplicación se limite a sistemas críticos, es decir, sistemas cuyo mal funcionamiento puede causar daños de magnitud, aunque los beneficios que sus técnicas proveen son relevantes a todo tipo de software. Poder trasladar los beneficios de los métodos formales a contextos de desarrollo de software más amplios que los sistemas críticos tendría un alto impacto en la productividad en tales contextos. Hipótesis. Contar con herramientas de análisis automático es un elemento de gran importancia. Ejemplos de esto son varias herramientas potentes de análisis basadas en métodos formales, cuya aplicación apunta directamente a código fuente. En la amplia mayoría de estas herramientas, la brecha entre las nociones a las cuales están acostumbrados los desarrolladores y aquellas necesarias para la aplicación de estas herramientas de análisis formal sigue siendo demasiado amplia. Muchas herramientas utilizan lenguajes de aserciones que escapan a los conocimientos y las costumbres usuales de los desarrolladores. Además, en muchos casos la salida brindada por la herramienta de análisis requiere cierto manejo del método formal subyacente. Este problema puede aliviarse mediante la producción de herramientas adecuadas. Otro problema intrínseco a las técnicas automáticas de análisis es cómo se comportan las mismas a medida que el tamaño y complejidad de los elementos a analizar crece (escalabilidad). Esta limitación es ampliamente conocida y es considerada crítica en la aplicabilidad de métodos formales de análisis en la práctica. Una forma de atacar este problema es el aprovechamiento de información y características de dominios específicos de aplicación. Planteo de objetivos. Este proyecto apunta a la construcción de herramientas de análisis formal para contribuir a la calidad, en cuanto a su corrección funcional, de especificaciones, modelos o código, en el contexto del desarrollo de software. Más precisamente, se busca, por un lado, identificar ambientes específicos en los cuales ciertas técnicas de análisis automático, como el análisis basado en SMT o SAT solving, o el model checking, puedan llevarse a niveles de escalabilidad superiores a los conocidos para estas técnicas en ámbitos generales. Se intentará implementar las adaptaciones a las técnicas elegidas en herramientas que permitan su uso a desarrolladores familiarizados con el contexto de aplicación, pero no necesariamente conocedores de los métodos o técnicas subyacentes. Materiales y métodos a utilizar. Los materiales a emplear serán bibliografía relevante al área y equipamiento informático. Métodos. Se emplearán los métodos propios de la matemática discreta, la lógica y la ingeniería de software. Resultados esperados. Uno de los resultados esperados del proyecto es la individualización de ámbitos específicos de aplicación de métodos formales de análisis. Se espera que como resultado del desarrollo del proyecto surjan herramientas de análisis cuyo nivel de usabilidad sea adecuado para su aplicación por parte de desarrolladores sin formación específica en los métodos formales utilizados. Importancia del proyecto. El principal impacto de este proyecto será la contribución a la aplicación práctica de técnicas formales de análisis en diferentes etapas del desarrollo de software, con la finalidad de incrementar su calidad y confiabilidad. A crucial factor for software quality is correcteness. Traditionally, formal approaches to software development concentrate on functional correctness, and tackle this problem basically by being based on well defined notations founded on solid mathematical grounds. This makes formal methods better suited for analysis, due to their precise semantics, but they are usually more complex, and require familiarity and experience with the manipulation of mathematical definitions. So, their acceptance by software engineers is rather restricted, and formal methods applications have been confined to critical systems. Nevertheless, it is obvious that the advantages that formal methods provide apply to any kind of software system. It is accepted that appropriate software tool support for formal analysis is essential, if one seeks providing support for software development based on formal methods. Indeed, some of the relatively recent sucesses of formal methods are accompanied by good quality tools that automate powerful analysis mechanisms, and are even integrated in widely used development environments. Still, most of these tools either concentrate on code analysis, and in many cases are still far from being simple enough to be employed by software engineers without experience in formal methods. Another important problem for the adoption of tool support for formal methods is scalability. Automated software analysis is intrinsically complex, and thus techniques do not scale well in the general case. In this project, we will attempt to identify particular modelling, design, specification or coding activities in software development processes where to apply automated formal analysis techniques. By focusing in very specific application domains, we expect to find characteristics that might be exploited to increase the scalability of the corresponding analyses, compared to the general case.

Dynamin-SNARE interactions control trans-SNARE formation in intracellular membrane fusion.

The fundamental processes of membrane fission and fusion determine size and copy numbers of intracellular organelles. Although SNARE proteins and tethering complexes mediate intracellular membrane fusion, fission requires the presence of dynamin or dynamin-related proteins. Here we study these reactions in native yeast vacuoles and find that the yeast dynamin homologue Vps1 is not only an essential part of the fission machinery, but also controls membrane fusion by generating an active Qa SNARE-tethering complex pool, which is essential for trans-SNARE formation. Our findings provide new insight into the role of dynamins in membrane fusion by directly acting on SNARE proteins.