Trabajo de Lógica Computacional en la Universidad de Yale

PorJosé A. Alonso

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

PorJosé A. Alonso

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)

PorJosé A. Alonso

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

PorJosé A. Alonso

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

PorJosé A. Alonso

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.