Trabajo de Lógica Computacional en Grenoble

PorJosé A. Alonso

Bull y el Centro de investigación INRIA de Grenoble Rhône-Alpes han ofertado un puesto de trabajo de 3 años para realizar una tesis doctoral.

El tema de la tesis es ”Vérification de protocoles de cohérence de caches pour les calculateurs à haute performance”.

El trabajo de la tesis consistirá en modelisar y verificar los protocolos de Bull, usando los métodos y herramientas existentes, chequeadores de modelos (CADP, Murphi, …) y/o sistemas de razonamiento (PVS, Coq, …), o combinaciones de dichas herramientas.

Más información en Bull et le Centre de recherche INRIA de Grenoble Rhône-Alpes recrutent un doctorant.

Trabajo en el Proyecto CerCo (Certified Complexity)

PorJosé A. Alonso

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:

  1. dos plazas para trabajar en el proyecto Cerco en París en el Laboratoire Preuves, Programmes et Systèmes.
  2. una plaza para trabajar en el proyecto CerCo en Bolonia en el . La verificación se hará con el sistema .