Jan Olaf Blech y Benjamin Grégoire han publicado el artículo Certifying compilers using higher-order theorem provers as certificate checkers en la revista Formal Methods in System Design.
El resumen del artículo es
Read More “Reseña: Certifying compilers using higher-order theorem provers as certificate checkers”
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.
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.
EL 29 de Octubre se publicó un nuevo artículo de vrificación: Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude, Science of Computer Programming en la revista Science of Computer Programming.
Los autores del artículo son Kyungmin Bae (de la University de Illinois en Urbana-Champaign), Peter Csaba Olveczky (de la Universidad de Oslo), Thomas Huining Feng, Edward A. Lee y Stavros Tripakis (los tres últimos, de la Universidad de California en Berkeley).
El resumen del artículo es
This paper defines a real-time rewriting logic semantics for a significant subset of Ptolemy II discrete-event models. This is a challenging task, since such models combine a synchronous fixed-point semantics with hierarchical structure, explicit time, and a rich expression language. The code generation features of Ptolemy II have been leveraged to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model, and to integrate Real-Time Maude verification of the synthesized model into Ptolemy II. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude. We illustrate such formal verification of Ptolemy II models with three case studies.
Una versión previa del artículo, de libre acceso, es Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude.
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.