|
Info de contacto
|
En qué ando
|
|
Sebastian Uchitel
suchitel@dc.uba.ar
LaFHIS – YPF
http://lafhis.dc.uba.ar/en/~suchitel
|
Ultimamente el foco está en:
1) Técnicas de Sintesis
aplicadas a Ing de Software y particularmente Sistemas
Adaptativos y Robots
2) Reliability (Analisis probabilistico)
|
|
Carlos Lopez Pombo
clpombo@dc.uba.ar
DC – FCEyN – UBA. THIS
|
Software orientado a servicios
|
|
Diego Garbervetsky
diego.garbervetsky@gmail.com
UBA - LaFHIS
http://lahifs.dc.uba.ar/~diegog
|
Análisis de Programas. Sobre todo estimación de
recursos. Algo de extracción de modelos de comportamiento,
algo de verificación automática, algo de testing, algo de
points-to analysis, empezando con algunos temas de
reliability.
|
|
Mariano Cerrutti
vscorza@gmail.com
UBA - LaFHIS
|
Estamos trabajando con un framework de ejecución de
planes que toma una especificación en una variante de FSP
para sintetizar un controlador y luego ejecutarlo a través
de adaptadores, en particular en un escenario con robots de
movimiento planar.
|
|
Tomas Scally
horizontedesucesos@gmail.com
LaFHIS
|
Estoy construyendo algoritmos
heuristicos para la eleccion del proximo objetivo a cumplir
en la fase de sintesis de controladores. La idea es maximizar
la cantidad de objetivos cumplidos minimizando la cantidad de
acciones realizadas.
Estoy diseñando distintas
estrategias y comparando los resultados.
Esto es mi trabajo de tesis de licenciatura.
|
|
Fernando Asteasuain
feraste@gmail
UBA - LaFHIS
|
Lenguajes declarativos para la especificación de
propiedades que modelan el comportamiento de un sistema.
Análisis del poder expresivo de los formalismos, y la
capacidad para llevar adelante la validación de la
especificación del comportamiento.
|
|
Dipi
dipi@dc.uba.ar
UBA – LaFHIS
http://www.doc.ic.ac.uk/~srdipi/
|
My research interests are mainly focused towards
behavioural modelling, partial behavioural modelling,
planning, controller synthesis and model checking.
|
|
Pablo Castro
pcastro@dc.exa.unrc.edu.ar
UNRC - MFIS
|
En este momento estoy
trabajando en:
* Especificación de
programas tolerantes a fallas,
* Verificación de programas
tolerantes a fallas,
* Síntesis de programas tolerantes a fallas
|
|
Germán Regis
gregis@dc.exa.unrc.edu.ar
UNRC - MFIS
Página
Personal
|
Actualmente trabajo en la aplicación de técnicas
formales (en particular model checking) para la
especificación y análisis de procesos de negocios.
Recientemente comenzado a pensar en métodos para
refinamiento o generación (sintesis) de workflows a partir
de especificaciones declarativas (lógicas modales).
|
|
Nicolás Ricci
nricci.02@gmail.com
UNRC - MFIS
|
Especificamente (y en este
momento): Definición de nociones de tolerancia a fallas en
un contexto probabilístico. Algorítmos de síntesis de
sistemas tolerantes a fallas.
Tópicos generales y/o trabajados en el pasado: Lógicas
modales, temporales, dinámicas, y con probabilidades.
|
|
Cecilia Kilmurray
ckilmurray@dc.exa.unrc.edu.ar
UNRC - MFIS
http://dc.exa.unrc.edu.ar/staff/ckilmurray
|
Trabajo principalmente en la
especificación y verificación de sistemas tolerantes a
fallas (lógicas modales, model checking, elems. de
probabilidades).
En este ultimo año estuve
estudiando una nueva clase de autómatas llamada p-automata.
Fruto de este estudio hemos desarrollado una extensión de la
lógica PCTL con un operador recursivo, lo cual aumenta la
expresividad de PCTL pero manteniendo la complejidad del
problema de model checking polinomial.
Justamente utilizamos
p-autómatas para darle semántica a esta nueva extensión de
la lógica, ya que cada fórmula es traducida a un p-automata
que acepta exactamente todas aquellas cadenas de Markov donde
vale dicha fórmula.
Creemos que la principal
aplicación de esta lógica, a la cual llamamos rPCTL, será
la abstracción y verificación de propiedades
probabilísticas de sistemas tolerantes a fallas, ya que los
operadores recursivos permiten justamente caracterizar muchas
de las nociones que aparecen en propiedades de tolerancia
falla,
como la de permanecer o visitar con cierta frecuencia una
región del sistema. La idea para los próximos meses es
implementar el algoritmo de model checker para rPCTL.
|
|
Nazareno Aguirre
naguirre@dc.exa.unrc.edu.ar
UNRC - MFIS
http://dc.exa.unrc.edu.ar/staff/naguirre/
|
Mi trabajo se centra
actualmente en el uso de SAT solving para analizar código o
modelos de software. Algunas de las tareas de análisis a las
que apuntamos son:
• Verificación de código
con anotaciones
• Análisis automático de
especificaciones de requisitos de software (e.g., SCR,
Clafer, KAOS)
• Generación automática
de tests unitarios
• Reparación automática
de programas
También trabajo en la definición de fundamentos
formales, basados en elementos de Teoría de Categorías,
para diferentes aspectos de lenguajes de especificaciones
formales, incluyendo la estructuración de especificaciones,
el refinamiento, y la reconfiguración dinámica.
|
|
Laura Brandán Briones
laura.brandan@gmail.com
FaMAF
|
Diagnosticabilidad y testing
|
|
Valeria Bengolea
vbengolea@dc.exa.unrc.edu.ar
UNRC - MFIS
|
Técnicas de reducción del espacio de búsqueda en la
generación exhaustiva acotada de casos de test para
estructuras complejas alojadas en memoria dinámica.
|
|
Renzo Degiovanni
rdegiovanni@dc.exa.unrc.edu.ar
UNRC – MFIS
|
Estoy interesado en aplicar
análisis automático a la tarea de validación de requisitos
de software, en lo posible utilizando SAT solving.
Recientemente desarrollamos una técnica para la
""operacionalización de goals"" basada
en SAT solving e Interpolación.
|
|
Christian Russo
christian.russo8@gmail.com
UBA - LaFHIS
|
Proyecto NXT Lego mindstorms.
|
|
Victor Braberman
vbraber@dc.uba.ar
UBA - LaFHIS
http://lafhis.dc.uba.ar/es/~vbraber
|
Síntesis de controladores, testing, análisis
cuantitativo (e.g., reliability, consumo de memoria), modelos
de comportamiento.
|
|
Paula Chocron
paulachocron@gmail.com
FCEN - THIS
|
Análisis modular en SMT solving
|
|
Marcelo Frias,
mfrias@itba.edu.ar
ITBA y CONICET
|
Análisis
y verificación de código utilizando SAT.
Generación
automática de Casos de Test utilizando SAT
Incremental.
Optimizaciones
para ejecución simbólica.
Localización
automática de fallas.
Reparación
automática de fallas.
|
|
Pedro R. D'Argenio
dargenio@famaf.unc.edu.ar
UNC - DSG
|
Confiabilidad,
Verificación, Model checking, Dependability.
Ver la página del
grupo para más info: http://dsg.famaf.unc.edu.ar
|
