Trabajo de Lógica Computacional en Grenoble
El grupo VDS (Verification & Modeling of Digital Systems Group) del Laboratorio TIMA (Techniques de l’Informatique et de la Microélectronique pour l’Architecture des systèmes intégrés) en Grenoble ha anunciado la ogerta de una plaza de trabajo: Formal methods for verifying dependability properties for a secured architecture.
El trabajo se desarrollará dentro del proyecto SHIVA (Secured Hardware Immune Versatile Architecture) y será dirigido por Laurence Pierre.
Los objetivos del trabajo serán la especificación de la propiedades de seguridad necesarias para los módulos hardware desarrollados por otros equipos del proyecto, la mejora de la especificación y de las metodologías de la verificación y su aplicación a las tareas verificadas.
Un precedente del trabajo es la verificación formal de comunicaciones en redes de chips con ACL2.