Reseña: Light-weight containers for Isabelle: efficient, extensible, nestable

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en Isabelle/HOL titulado Light-weight containers for Isabelle: efficient, extensible, nestable.

Su autor es Andreas Lochbihler (del ETH Zürich).

El trabajo se presentará en julio en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

In Isabelle/HOL, we develop an approach to efficiently implement container types such as sets and maps in generated code. Thanks to type classes and refinement during code generation, our light-weight framework is flexible, extensible, and easy to use. To support arbitrary nesting of containers, we devise an efficient linear order on sets that can even compare complements and non-complements. Our evaluation shows that it is both efficient and usable.

Los códigos de las correspondientes teorías en Isabelle/HOL se encuentran aquí.

RA2012: Verificación de propiedades de la sustitución en Isabelle/HOL

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha resuelto de manera colaborativa ejercicios sobre la demostración de propiedades de la función de sustitución con Isabelle/HOL. Su objetivo es ilustrar el uso del razonamiento por inducción y por casos en Isabelle. Para ca propiedad se presentan distintas demostraciones desde las automáticas a las detalladas.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Verificación de propiedades de la sustitución en Isabelle/HOL”

Reseña: Graph theory

PorJosé A. Alonso

Se ha publicado un nuevo artículo de razonamiento formalizado en Isabelle/HOL titulado Graph theory.

Su autor es Lars Noschinski (de la Univrsidad Técnica de Munich).

Su resumen es

This development provides a formalization of directed graphs, supporting (labelled) multi-edges and infinite graphs. A polymorphic edge type allows edges to be treated as pairs of vertices, if multi-edges are not required. Formalized properties are i.a. walks (and related concepts), connectedness and subgraphs and basic properties of isomorphisms.

This formalization is used to prove characterizations of Euler Trails, Shortest Paths and Kuratowski subgraphs.

Definitions and nomenclature are based on Digraphs: Theory, algorithms and applications (by J. Bang-Jensen and G. Gutin).

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

RA2012: Razonamiento sobre programas con Isabelle/HOL (2)

PorJosé A. Alonso

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha continuado la presentación (iniciada en la clase anterior) de cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL.

En la presentación se han usado los ejemplos del tema 8 del curso de Informática (de 1º del Grado en Matemáticas).

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Razonamiento sobre programas con Isabelle/HOL (2)”