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.

Interactive Proof: Introduction to Isabelle/HOL

PorJosé A. Alonso

Tobias Nipkow ha publicado un nuevo tutorial de Isabell/HOL: Interactive Proof: Introduction to Isabelle/HOL, que presentará a principio de agosto en la Summer School Marktoberdorf 2011.

El contenido del tutorial es el siguiente:

  • Elementos básicos de Isabelle/HOL: los tipos, términos, fórmulas y teorías.
  • Isabelle/HOL como lenguaje funcional verificable. En esta sección, presenta los tipos básicos (bool, nat y list), cómo pueden definirse funciones y tipos y cómo pueden demostrarse propiedades por inducción y simplificación.
  • Lógica y automatización de las demostraciones. En esta sección, presenta cómo se trabaja con fórmulas y conjuntos, cómo puede automatizarse las demostraciones de sus propiedades y cómo pueden analizarse las demostraciones en pasos elementales.
  • Demostraciones estructuradas con Isar. En esta sección, presenta ejemplos de demostraciones en Isar, patrones de demostraciones, técnicas para mejorar demostraciones y demostraciones por inducción y casos en Isar.

La presentación del tutorial está basada en ejemplos: se concentra en ejemplos que presenta los casos típicos sin explicar el caso general si se puede inferir de los ejemplos.

Las teorías que sirven de ejemplo del tutorial son las siguientes: Overview, Nat, List, Tree, Simp, Induct, Auto_Proof_Demo, Single_Step_Demo, Inductive_Demo, Isar_Demo, Isar_Induct_Demo.

El resto del material utilizado se encuentra en MOD2011.

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).

RA2010: Investigación en lógica computacional

PorJosé A. Alonso

Las clases de esta semana del curso de Razonamiento automático se han sustituido por las conferencias de las Jornadas de Lógica, Computación e Inteligencia Artificial

En dichas Jornadas, he presentado las investigaciones en Lógica
computacional realizadas por el Grupo de Lógica Computacional de la Universidad de Sevilla.

El título de la presentación fue Lógica Computacional en Sevilla (30 años en una hora).
Read More “RA2010: Investigación en lógica computacional”