Menu Close

Categoría: Trabajo

Ofertas de trabajos en Lógica Computacional.

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.

Trabajo de Lógica Computacional en la Universidad de Yale

El Departamento de Ciencias de la Computación de la Universidad de Yale
ha pubicado una oferta de trabajo en temas de Lógica Computacional: PostDoc and PhD Positions at Yale University

El objetivo del trabajo es el desarrollo de un nuevo sistema operativo cuyo núcleo esté formalmente certificado. Una descripción detallada del mismo se encuentra en Advanced Development of Certified OS Kernels.

El trabajo se desarrollará en el grupo FLINT y será dirigido por Zhong Shao y Bryan Ford.

Trabajo de lógica computacional en Kassel

El Grupo de Métodos Formales y Verificación de la Universidad de Kassel, Alemania, ha publicado el anuncio de la oferta de una plaza postdoctoral para trabajar en lógica computacional.

El trabajo se desarrollará en el proyecto ERC Model Checking Unleashed.

El objetivo del trabajo es el estudio de aplicaciones no estándard de las técnicas de verificación de modelos (en inglés, model checking) en varias áreas de ciencias de la verificación y temas relacionados.

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 un anuncio de ofertas de plazas.

La investigación del grupo se centra en la deducción automática en fragmentos de la lógica de primer orden.

Desde el punto de vista teórico trabajan en el desarrollo, análisis y combinación de cálculos lógicos.

Desde el punto de vista práctico trabajan en la implementación de demostradores automáticos de teoremas y otros sistemas deductivos y su aplicación a la verificación asistida por computador de software y hardware.

Algunos de los sistemas que desarrolla el grupo son SPASS, SPASS+T y Waldmeister

Trabajo de Lógica Computacional en Cambridge

Se ha anunciado la oferta de plazas de trabajo en la Universidad de Cambridge.

El trabajo se realizará dentro del proyecto EPRSC Semantic Foundations for Real-World Systems. Entre sus objetivos se encuentra la verificación de la compilación de lenguajes concurrentes, para lo que se requiere conocimiento de verificación de programas y de sistemas de razonamiento.

El director del proyecto es Peter Sewell

Trabajo de Lógica Computacional en las Universidades de Pensilvania, Harvard y Northeastern

Se ha anunciado la oferta de plazas postdoctorales en la Universidad de Pensilvania, la Universidad de Harvard y la Universidad Northeastern.

El trabajo se desarrollará dentro del proyecto SAFE (Semantically Aware Foundation Environment).

SAFE es parte del proyecto CRASH (Clean-Slate Design of Resilient, Adaptive, Secure Hosts)

CRASH es un gran proyecto financiado por la DARPA (Defense Advanced Research Projects Agency) cuyo objetivo es el diseño de nuevos sistemas computacionales que sean muy resistentes a los ciberataques. Se desea diseñar los niveles de hardware, sistemas operativos y lenguajes de programación poniendo el énfasis en la simplicidad, seguridad y verificabilidad de todos los niveles.

Las áreas de trabajo son lenguajes de programación, verificación formal, sistemas operativos y diseño de hardware.