Open project position at TUM: Computer-supported verification of automata constructions

El grupo Foundations of Software Reliability and Theoretical Computer Science de la Universidad Politécnica de Munich ha anunciado la oferta de una plaza de trabajo en Lógica Computacional: Open project position at TUM: Computer-supported verification of automata constructions

El objetivo del trabajo es la realización de una biblioteca formalmente verificada con Isabelle de algoritmos de verificación de modelos (en inglés, model checking). El proyecto se enfoca en la aproximación a la verificación de modelos basada en automata. Por tanto, para su realización se será necesario formalizar en Isabelle los conceptos habituales de la teoría de automata.

Los directores del proyecto son Javier Esparza, Tobias Nipkow y Jan-Georg Smaus.

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.

Trabajo de Lógica Computacional en Saarbrücken (Alemania)

El Grupo de automatización de la Lógica (del Instituto Max Planck en Saarbrücken, Alemania) ha publicado una oferta de plaza: PhD/Project Position.

La investigación se centrará en la integración de un sistema de razonamiento automático (SPASS) con otro interactivo (Isabelle).

El trabajo será dirigido por Christoph Weidenbach y se desarrollará en cooperación con el Grupo de demostración automática de la Universidad de Munich que dirige Tobias Nipkow.

Trabajo de Lógica Computacional en Enschede (Países Bajos)

El Grupo de métodos formales de la Universidad de Twente ha ofertado 2 plazas para trabajar en Enschede (Países Bajos): PhD and Post Doc position on ERC project Verifcation of Concurrent Data Structures (U. Twente, Netherlands)

El trabajo consistirá en la especificación y verificación de estructuras de datos concurrentes.

Las dos plazas se incriben en el proyecto VerCors (Verification of Concurrent Data Structures) dirigido por Marieke Huisman.