Se busca estudiante de ciencias de la computación o licenciatura en matemática interesado en hacer un doctorado, solicitando una beca en la próxima convocatoria del CONICET, en cotutela con investigadores franceses. 

Lugar de trabajo: Centro Internacional Franco Argentino de Ciencias de la Información y de Sistemas, CIFASIS (con posibles estadías cortas anuales en el INRIA Saclay de Francia).

Investigadores responsables: Maximiliano Cristiá y Ricardo Katz.

Tema: El tema de investigación se inscribe dentro de pruebas formales de propiedades y algoritmos relacionados a poliedros, tanto en el contexto clásico como 
en el tropical. Este es un tema de investigación interdisciplinario entre ciencias de la computación y matemática.

Descripción: Por pruebas formales de propiedades y algoritmos entendemos el uso de lenguajes de especificación formal y de asistentes de prueba capaces de demostrar teoremas en esos lenguajes. Un asistente de pruebas es un software que se utiliza para realizar y verificar cada paso de una demostración. En particular, algunos asistentes (como Coq) permiten además obtener programas que implementan las propiedades demostradas.

Los poliedros juegan un rol importante en varias aplicaciones. Por ejemplo, se usan en la verificación de software porque permiten estimar el rango de variación de las variables del programa y así comprobar si toman valores admisibles. Con este fin también se han utilizado los poliedros tropicales, que son los análogos de los poliedros clásicos en la estructura algebraica que se obtiene al considerar el conjunto de los números reales con el máximo como suma de dos números y la suma habitual como su multiplicación (en algunas casos, los poliedros tropicales proporcionan mejores resultados que los clásicos). Otra aplicación de los poliedros se presenta en la verificación de propiedades de safety para sistemas de eventos discretos.

Dado que algunas de estas aplicaciones son críticas, es necesario disponer de software formalmente verificado de manera tal de que no se produzcan errores.

Los interesados pueden comunicarse por e-mail a:
Maximiliano Cristiá: Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
Ricardo Katz: Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.