Menu Close

Etiqueta: Isabelle/HOL

Reseña: Numerical analysis of ordinary differential equations in Isabelle/HOL

El miércoles (15 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Isabelle/HOL titulado Numerical analysis of ordinary differential equations in Isabelle/HOL

Sus autores son Fabian Immler y Johannes Hölzl (de la Technische Universität München).

El resumen del trabajo es

Many ordinary differential equations (ODEs) do not have a closed solution, therefore approximating them is an important problem in numerical analysis. This work formalizes a method to approximate solutions of ODEs in Isabelle/HOL.

We formalize initial value problems (IVPs) of ODEs and prove the existence of a unique solution, i.e. the Picard-Lindelöf theorem. We introduce generic one-step methods for numerical approximation of the solution and provide an analysis regarding the local and global error of one-step methods.

We give an executable specification of the Euler method as an instance of one-step methods. With user-supplied proofs for bounds of the differential equation we can prove an explicit bound for the global error. We use arbitrary-precision floating-point numbers and also handle rounding errors when we truncate the numbers for efficiency reasons.

El código de la formalización en Isabelle/HOL se encuentra aquí.

Reseña: Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL

Se ha publicado un trabajo de razonamiento formalizado en Isabelle/HOL, titulada Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL.

Su autor es Jose Divasón Mallagaray, dirigido por Jesús María Aransay Azofra (de la Univ. de la Rioja).

La presentación del trabajo tuvo lugar el 25 de Octubre de 2011 en la Universidad de la Rioja.

El objetivo del trabajo es la formalización en Isabelle/HOL de conceptos y teoremas sobre álgebra lineal siguiendo la 16 primeras secciones del libro de Halmos Finite-dimensional vector spaces.

El resumen del trabajo es

In this work we deal with finite-dimensional vector spaces over a generic field \mathbb{K}. First we will state properties of vector spaces independently of their dimension. Then, we will introduce the conditions to obtain finite-dimensional vector spaces. The notions of linear dependence and independence, as well as linear combinations, and hence the notion of basis will be presented. Some results about the dimension of the different basis of a vector space will be necessary, as well as on the isomorphism among vector spaces. Once we have introduced the notion of basis, and with the additional condition of it being finite, we will introduce the notion of finite-dimensional vector space. Next step is to introduce vector subspaces. We will pay attention to vector susbpaces generated by a given set of vectors and prove some of their properties. The notion of linear maps will be also required to define isomorphisms of vector spaces. Finally, we will prove that a vector space (over a field \mathbb{K}) of (finite) dimension n is isomorphic to \mathbb{K}^n.

The previous results will be presented following the book by Halmos on vector spaces [1]. Its formalization will be carried out in Isabelle/HOL.

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

Una extensión del trabajo es Formalizing an abstract algebra textbook in Isabelle/HOL presentado el 14 de junio de 2012 en el EACA 2012 (EACA 2012
XIII Encuentro de Álgebra Computacional y Aplicaciones).

Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.

Reseña: Correctness of pointer manipulating algorithms illustrated by a verified BDD construction

Se ha publicado un nuevo trabajo de verificación formal en Isabelle/HOL titulado Correctness of pointer manipulating algorithms illustrated by a verified BDD construction.

Los autores del trabajo son Mathieu Giorgino y Martin Strecker (de la Univ. de Toulouse).

El trabajo se presentará el 29 de agosto en el FM 2012 (18th International Symposium on Formal Methods).

En el trabajo se presenta una metodología para la verificación de programas imperativos usando el asistente de prueba Isabelle/HOL y su extensión Imperative_HOL, junto con el generador de código Scala de Isabelle. Como aplicación de la metodología se verifica los diagramas de decisión binarios (BDD).

Su resumen es

This paper is an extended case study using a high-level approach to the verification of graph transformation algorithms: To represent sharing, graphs are considered as trees with additional pointers, and algorithms manipulating them are essentially primitive recursive traversals written in a monadic style. With this, we achieve almost trivial termination arguments and can use inductive reasoning principles for showing the correctness of the algorithms. We illustrate the approach with the verification of a BDD package which is modular in that it can be instantiated with different implementations of association tables for node lookup. We have also implemented a garbage collector for freeing association tables from unused entries. Even without low-level optimizations, the resulting implementation is reasonably efficient.

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

El trabajo es parte del proyecto CLIMT (Categorical and Logical Methods in Model Transformation).

Reseña: Algorithms in games evolving in time: Winning strategies based on testing

Se ha publicado un nuevo artículo de razonamiento formalizado en Isabelle/HOL sobre la teoría de juegos, titulado Algorithms in games evolving in time: Winning strategies based on testing. Sus autores son Evgeny Dantsin, Jan-Georg Smaus y Sergei Soloviev y se presentará el 12 de agosto en el Isabelle Users Workshop 2012.

Su resumen es

We model two-player imperfect-information games evolving in time, where one player makes and tests “hypotheses” about the opponent’s strategies. We consider algorithms needed for the first player to compute a winning strategy. The main assumptions about the scenario are the following: (1) the hypotheses form a “covering”, i.e., each strategy of the second player satisfies at least one hypothesis; (2) the hypotheses can be enumerated and tested; (3) for each hypothesis, the first player has a strategy that “defeats” all of the opponent’s strategies satisfying this hypothesis.

We have modelled a significant part of the theory presented here in Isabelle/HOL.

Reseña: Lifting and transfer: A modular design for quotients in Isabelle/HOL

Se ha publicado un nuevo artículo sobre automatización del razonamiento en Isabelle/HOL: Lifting and transfer: A modular design for quotients in Isabelle/HOL.

Sus autores son Brian Huffman y Ondřej Kunčar (de la Technische Universität München).

El trabajo se presentará el 12 de agosto en el Isabelle Users Workshop 2012 en el marco del ITP 2012 (third conference on Interactive Theorem Proving).

Su resumen es

Quotients, subtypes, and other forms of type abstraction are ubiquitous in formal reasoning with higher-order logic. Typically, users want to build a library of operations and theorems about an abstract type, but they want to write definitions and proofs in terms of a more concrete representation type, or “raw” type. Earlier work on the Isabelle Quotient package [1, 2] has yielded great progress in automation, but it still has many technical limitations.

We present an improved, modular design centered around two new packages: the Transfer package for proving theorems, and the Lifting package for defining constants. Our new design is simpler, applicable in more situations, and has more user-friendly automation. An initial implementation is available in Isabelle 2012.

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.

Interactive Proof: Introduction to Isabelle/HOL

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

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

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