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

PorJosé A. Alonso

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: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization

PorJosé A. Alonso

Esta semana se ha publicado en el Journal of Automated Reasoning un nuevo artículo de razonamiento formalizado en PVS: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization. Una versión previa se puede leer libremente aquí.

Los autores son César Muñoz y Anthony Narkawicz de NASA Langley Formal Methods.

Su resumen es

This paper presents a formalization in higher-order logic of an efficient representation of multivariate Bernstein polynomials. Using this representation, an algorithm for finding lower and upper bounds of the minimum and maximum values of a polynomial has been formalized and verified correct in the Prototype Verification System (PVS). The algorithm is used in the definition of proof strategies for formally and automatically solving polynomial global optimization problems.

Reseña: Rigorous polynomial approximation using Taylor models in Coq

PorJosé A. Alonso

Se ha publicado un nuevo artículo de razonamiento formalizado en Coq sobre cálculo numérico: Rigorous polynomial approximation using Taylor models in Coq.

Sus autores son Nicolas Brisebarre, Mioara Maria Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca,
Laurence Rideau y Laurent Théry. Todos son miembros del grupo CoqApprox.

El trabajo se ha desarrollado dentro del proyecto TaMaDi y se presentó el 5 de abril en el NFM 2012 (4th NASA Formal Methods Symposium).

El resumen del trabajo es

One of the most common and practical ways of representing a real function on machines is by using a polynomial approximation. It is then important to properly handle the error introduced by such an approximation. The purpose of this work is to offer guaranteed error bounds for a specific kind of rigorous polynomial approximation called Taylor model. We carry out this work in the Coq proof assistant, with a special focus on genericity and efficiency for our implementation. We give an abstract interface for rigorous polynomial approximations, parameterized by the type of coefficients and the implementation of polynomials, and we instantiate this interface to the case of Taylor models with interval coefficients, while providing all the machinery for computing them. We compare the performances of our implementation in Coq with those of the Sollya tool, which contains an implementation of Taylor models written in C. This is a milestone in our long-term goal of providing fully formally proved and efficient Taylor models.

Este trabajo es continuación de la tesis doctoral de Mioara Joldes titulada Rigorous polynomial approximations and applications, dirigida por Nicolas Brisebarre y Jean-Michel Muller presentada el 26 de septiembre de 2011 en la Universidad de Lyon.

El código de las teorías correspondientes al trabajo 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.