Reseña: Square root and division elimination in PVS

PorJosé A. Alonso

Se ha publicado un artículo de automatización del razonamiento en PVS titulado Square root and division elimination in PVS.

Su autor es Pierre Neron (del INRIA en Paris – Rocquencourt).

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

Su resumen es

In this paper we present a new strategy for PVS that implements a square root and division elimination in order to use automatic arithmetic strategies that were not able to deal with these operations in a first place. This strategy relies on a PVS formalization of the square root and division elimination and deep embedding of PVS expressions inside PVS. Therefore using computational reflection and symbolic computation we are able to automatically transform expressions into division and square root free ones before using these decisions procedures.

El código de las correspondientes teorías PVS se encuentra aquí.

Reseña: One logic to use them all

PorJosé A. Alonso

Una de las principales barreras en el avance de la automatización del razonamiento consiste en la comunicación entre distintos sistemas de razonamiento. Una forma de superarla es la planteada en el artículo One logic to use them all.

Su autor es Jean-Christophe Filliâtre (de la Universidad de París-Sur).

El trabajo se presentará en el CADE-24 (24th International Conference on Automated Deduction).

Su resumen es

Deductive program verification is making fast progress these days. One of the reasons is a tremendous improvement of theorem provers in the last two decades. This includes various kinds of automated theorem provers, such as ATP systems and SMT solvers, and interactive proof assistants. Yet most tools for program verification are built around a single theorem prover. Instead, we defend the idea that a collaborative use of several provers is a key to easier and faster verification. This paper introduces a logic that is designed to target a wide set of theorem provers. It is an extension of first-order logic with polymorphism, algebraic data types, recursive definitions, and inductive predicates. It is implemented in the tool Why3, and has been successfully used in the verification of many non-trivial programs.

Reseña: Automating inductive proofs using theory exploration

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento automático sobre programas funcionales en Haskell titulado Automating inductive proofs using theory exploration.

Sus autores son Koen Claessens, Moa Johansson, Dan Rosén y Nicholas Smallbone (de la Universidad de Chalmers).

El trabajo se presentará en el CADE-24 (24th International Conference on Automated Deduction).

Su resumen es

HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.

El código de HipSpec se encuentra en aquí. Los experimentos con HipSpec se encuentran aquí.

LMF2013: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL (2)

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se han resuelto los ejercicios 22, 27, 28, 29, 32 y 34 de la relación 7 sobre deducción natural en lógica de primer orden con Isabelle/HOL.

Las soluciones de los ejercicios resueltos se muestran a continuación:
Read More “LMF2013: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL (2)”

Reseña: A fully verified executable LTL model checker

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado A fully verified executable LTL model checker.

Sus autores son Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf y Jan-Georg Smaus.

El trabajo se presentará en el CAV 2013 (25th International Conference on Computer Aided Verification).

Su resumen es

We present an LTL model checker whose code has been completely verified using the Isabelle theorem prover. The checker consists of over 4000 lines of ML code. The code is produced using recent Isabelle technology called the Refinement Framework, which allows us to split its correctness proof into (1) the proof of an abstract version of the checker, consisting of a few hundred lines of “formalized pseudocode”, and (2) a verified refinement step in which mathematical sets and other abstract structures are replaced by implementations of efficient structures like red-black trees and functional arrays. This leads to a checker that, while still slower than unverified checkers, can already be used as a trusted reference implementation against which advanced implementations can be tested. We report on the structure of the checker, the development process, and some experiments on standard benchmarks.

El trabajo forma parte del proyecto CAVA (Computer Aided Verification of Automata).

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