CAV (Computer Aided Verification) es una serie de congresos dedicados a la verificación asistida por ordenador de sistemas sofware y hardware. Este año se celebra el CAV 2010 en la Universidad de Edimburgo del 15 al 19 de Julio. La fecha para enviar artículos termina el 11 de Enero.
Se ha convocado una plaza de trabajo para realizar el doctorado en el Proyecto ForMath. El trabajo se realizará en el Foundations Group del Institute for Computing and Information Sciences de la Radboud University Nijmegen de Holanda.
El proyecto ForMath (Formalization of Mathematics) es un proyecto FP7 liderado por Thierry Coquand de la Gothenburg University. El objetivo del proyecto es desarrollar teorías formalizadas sobre álgebra, álgebra lineal, computación sobre los números reales y topología algebraica.
Se ha convocado dos plazas para trabajar en el Proyecto Cerco (Certified Complexity).
El proyecto Cerco es un Proyecto FP7 cuyo objetivo es la construcción de un compilador de C que conserve la complejidad y esté formalmente verificado. El proyecto se describe más detalladamente en su memoria.
Las plazas convocadas son:
CSL (Computer Science Logic) es el congreso anual de la EACSL (European Association for Computer Science Logic). El tema fundamental del congreso es la interrelación entre lógica y computación.
El CSL 2010 se celebrará en Brno (República Checa) el 23 de Agosto. El plazo de envío termina el 26 de marzo.
Una de las líneas de desarrollo de la Lógica Computacional es abordar formalizaciones de resultados matemáticos complejos. El intento de formalización produce como efectos laterales la formalización del conocimiento implícito en el resultado (el mathware) y el desarrollo de nuevos procedimientos de decisión.
Uno de los grandes retos actuales es la formalización de la demostración de Andrew Wiles del último teorema de Fermat. Una descripción detallada del reto se encuentra en el artículo Computer verification of Wiles’ proof of Fermat’s Last Theorem de Wim H. Hesselink. En el artículo se traza la hoja de ruta de la formalización describiendo la estructura de la demostración de Wiles. Una de las principales dificultades radica en comentando la necesidad de disponer de sistemas de razonamiento que incorporen cálculo simbólico. Hesselink estima que se tardarán unos 50 años en conseguirse la formalización del teorema de Wiles.