I1M2011: Examen final
Hoy se ha realizado el examen de la convocatoria de julio de Informática de 1º del Grado en Matemáticas
A continuación se muestra el examen junto con su solución:
Read More “I1M2011: Examen final”
Reseña: Rigorous polynomial approximation using Taylor models in Coq
Se ha publicado un nuevo artículo de razonamiento formalizado en Coq sobre cálculo numérico: Rigorous polynomial approximation using Taylor models in Coq.
Sus autores son Nicolas Brisebarre, Mioara Maria Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca,
Laurence Rideau y Laurent Théry. Todos son miembros del grupo CoqApprox.
El trabajo se ha desarrollado dentro del proyecto TaMaDi y se presentó el 5 de abril en el NFM 2012 (4th NASA Formal Methods Symposium).
El resumen del trabajo es
One of the most common and practical ways of representing a real function on machines is by using a polynomial approximation. It is then important to properly handle the error introduced by such an approximation. The purpose of this work is to offer guaranteed error bounds for a specific kind of rigorous polynomial approximation called Taylor model. We carry out this work in the Coq proof assistant, with a special focus on genericity and efficiency for our implementation. We give an abstract interface for rigorous polynomial approximations, parameterized by the type of coefficients and the implementation of polynomials, and we instantiate this interface to the case of Taylor models with interval coefficients, while providing all the machinery for computing them. We compare the performances of our implementation in Coq with those of the Sollya tool, which contains an implementation of Taylor models written in C. This is a milestone in our long-term goal of providing fully formally proved and efficient Taylor models.
Este trabajo es continuación de la tesis doctoral de Mioara Joldes titulada Rigorous polynomial approximations and applications, dirigida por Nicolas Brisebarre y Jean-Michel Muller presentada el 26 de septiembre de 2011 en la Universidad de Lyon.
El código de las teorías correspondientes al trabajo se encuentra aquí.
Reseña: A framework for formally verifying software transactional memory algorithms
Se ha publicado un nuevo artículo de verificación con PVS:
A framework for formally verifying software transactional memory algorithms que se presentará el 3 de Septiembre en CONCUR 2012 (23rd International Conference on Concurrency Theory).
Sus autores son Mohsen Lesani, Victor Luchangco y Mark Moir. El primero trabaja en UCLA y los restantes en Oracle.
El resumen del artículo es
We present a framework for verifying transactional memory (TM) algorithms. Specifications and algorithms are specified using I/O automata, enabling hierarchical proofs that the algorithms implement the specifications. We have used this framework to develop what we believe is the first fully formal machine-checked verification of a practical TM algorithm: the NOrec algorithm of Dalessandro, Spear and Scott.
Our framework is available for others to use and extend. New proofs can leverage existing ones, eliminating significant work and complexity.
Reseña: Large-scale formal verification in practice: A process perspective
Una de los proyectos más importante en verificación formal es el seL4 (Secure Microkernel Project) cuyo objetivo es la verificación con Isabelle/HOL del micronúcleo de S.O. seL4.
El 7 de junio, se presentó en el ICSE 2012 (34th International Conference on Software Engineering) un panorama del proyecto sel4: Large-scale formal verification in practice: A process perspective.
Sus autores son June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He (Jason) Zhang y Liming Zhu del NICTA (National ICT Australia Ltd).
Su resumen es
The L4 verified project was a rare success in large-scale, formal verification: it provided a formal, machine-checked, code-level proof of the full functional correctness of the seL4 microkernel. In this paper we report on the development process and management issues of this project, highlighting key success factors. We formulate a detailed descriptive model of its middle-out development process, and analyze the evolution and dependencies of code and proof artifacts. We compare our key findings on verification and re-verification with insights from other verification efforts in the literature. Our analysis of the project is based on complete access to project logs, meeting notes, and version control data over its entire history, including its long-term, ongoing maintenance phase. The aim of this work is to aid understanding of how to successfully run large-scale formal software verification projects.