Reseña: Mechanization of an algorithm for deciding KAT terms equivalence

PorJosé A. Alonso

Se ha publicado un nuevo trabajo sobre verificación formal en Coq: Mechanization of an algorithm for deciding KAT terms equivalence.

Sus autores son Nelma Moreira, David Pereira y Simao Melo de Sousa (de la Universidade do Porto, Portugal).

Su resumen es

This work presents a mechanically verified implementation of an algorithm for deciding the (in-)equivalence of Kleene algebra with tests (KAT) terms. This mechanization was carried out in the Coq proof assistant. The algorithm decides KAT terms equivalence through an iterated process of testing the equivalence of their partial derivatives. It is a purely syntactical decision procedure and so, it does not construct the underlying automata. The motivation for this work comes from the possibility of using KAT encoding of propositional Hoare logic for reasoning about the partial correctness of imperative programs.

El código de la formalización en Coq se encuentra aquí.

Reseña: A framework for formally verifying software transactional memory algorithms

PorJosé A. Alonso

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

PorJosé A. Alonso

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.

Reseña: Compositional verification of a communication protocol for a remotely operated aircraft

PorJosé A. Alonso

La semana pasada se publicó un nuevo artículo de verificación formal con PVS: Compositional verification of a communication protocol for a remotely operated aircraft.

Los autores del artículo son Alwyn E. Goodloe and César A. Muñoz.

El resumen del artículo es

This paper presents the formal specification and verification of a communication protocol between a ground station and a remotely operated aircraft. The protocol can be seen as the vertical composition of protocol layers, where each layer performs input and output message processing, and the horizontal composition of different processes concurrently inhabiting the same layer, where each process should satisfy a distinct delivery requirement. A compositional technique is used to formally prove that the protocol satisfies these requirements. Although the protocol itself is not novel, the methodology employed in its verification extends existing techniques by automating the tedious and usually cumbersome part of the proof, thereby making the iterative design process of protocols feasible.

En la Red se publicó una versión preliminar del artículo.

ProofWiki y la verificación de las demostraciones matemáticas

PorJosé A. Alonso

ProofWiki es un compendio de demostraciones matemáticas escritas de manera colaborativa en una wiki. Su objetivo es colecionar y clasificar demostraciones de teoremas matemáticos.

El proyecto empezó en marzo de 2008 y actualmente incluye 2.804 demostraciones escritas por sus 297 usuarios. Las demostraciones se encuentran clasificadas en 34 categorías. Una de las categorías particularmente interesante es la de teoremas con nombres en la que aparecen 247 teoremas. También es interesante la página de los teoremas más populares según el número de visitas.

ProofWiki podría servir de base para otro proyecto cuyo objetivo final fuese la verificación formal de las demostraciones matemáticas. Para ello se podría crear una wiki y, de forma colaborativa, escribir las verificaciones de las demostraciones de ProofWiki usando los distintos sistemas de razonamiento asistido por ordenador (como Isabelle/HOL/Isar, PVS, ACL2, Coq, HOL, HOL Light o Mizar).