Reseña: Interactive and automated proofs for graph transformations

PorJosé A. Alonso

Se ha publicado un trabajo de razonamiento formalizado en Isabelle/HOL titulado Interactive and automated proofs for graph transformations.

Su autor es Martin Strecker (de la Univ. Paul Sabatier, Toulouse, Francia).

Su resumen es

This article explores methods to provide computer support for reasoning about graph transformations. We first define a general framework for representing graphs, graph morphisms and single graph rewriting steps. This setup allows for interactively reasoning about graph transformations. In order to achieve a higher degree of automation, we identify fragments of the graph description language in which we can reduce reasoning about global graph properties to reasoning about local properties, involving only a bounded number of nodes, which can be decided by Boolean satisfiability solving or even by deterministic computation of low complexity.

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

Reseña: Operational refinement for compiler correctness

PorJosé A. Alonso

Este mes (septiembre de 2012) se va a presentar en la Universidad de Princeton una tesis doctoral de verificación formal en Coq titulada Operational refinement for compiler correctness.

Su autor es Robert W. Dockins, dirigido por Andrew W. Appel.

Su resumen es

Compilers are an essential part of the software development process. Programmers all over the world rely on compilers every day to correctly translate their intentions, expressed as high-level source code, into executable low-level machine code. But what does it mean for a compiler to be correct?

This question is surprisingly difficult to answer. Despite the fact that various groups have made concerted efforts to prove the correctness of compilers since at least the early 1980’s, no clear consensus has arisen about what it means for a compiler to be correct. As a result, it seems that no two compiler verification efforts have stated their correctness theorems in the same way.

In this dissertation, I will advance a new approach to compiler correctness based on refinements of the operational semantics of programs. The cornerstones of this approach are behavioral refinement, which allows programs to improve by going wrong less often, and choice refinement, which allows compilers to reduce the amount of internal nondeterminism present in a program. I take particular care to explain why these notions of refinement are the correct formal interpretations of the informal ideas above.

In addition, I will show how these notions of refinement can be realistically applied to compiler verification efforts. First, I will present a toy language, WHILE-C, and show how choice and behavioral refinement can be used to verify the correctness of several interesting program transformations. The WHILE-C language and the transformations themselves are simple enough to be presented here in full detail. I will also show how the ideas of behavioral and choice refinement may be applied to the CompCert formally verified compiler [Ler09a], a realistic compiler for a significant subset of C

El código Coq correspondiente a la tesis se encuentra aquí.

Esta tesis se enmarca en el proyecto Verified Software Toolchain.

Reseña: Formalization and verification of number theoretic algorithms using the Mizar proof checker

PorJosé A. Alonso

En el FCS’12 (The 2012 International Conference on Foundations of Computer Science) se presentó un trabajo de razonamiento formalizado en Mizar titulado Formalization and verification of number theoretic algorithms using the Mizar proof checker.

Sus autores son Hiroyuki Okazaki, Yoshiki Aoki y Yasunari Shidama (de la Shinshu University).

Su resumen es

In this paper, we introduce formalization of well-known number theoretic algorithms on the Mizar proof checking system. We formalized the Euclidean algorithm, the extended Euclidean algorithm and the algorithm computing the solution of the Chinese reminder theorem based on the source code of NZMATH which is a Python based number theory oriented calculation system. We prove the accuracy of our formalization using the Mizar proof checking system as a formal verification tool.

Reseña: Deriving a fast inverse of the generalized Cantor N-tupling bijection

PorJosé A. Alonso

La semana que viene (6 de septiembre) se presentará en el ICLP’12 (28th International Conference on Logic Programming) un trabajo sobre resolución lógica de problemas combinatorios titulado Deriving a fast inverse of the generalized Cantor N-tupling bijection.

Su autor es Paul Tarau (de la University of North Texas, Denton, Texas, USA).

Su resumen es

We attack an interesting open problem (an efficient algorithm to invert the generalized Cantor N-tupling bijection) and solve it through a sequence of equivalence preserving transformations of logic programs, that take advantage of unique strengths of this programming paradigm. An extension to set and multiset tuple encodings, as well as a simple application to a “fair-search” mechanism illustrate practical uses of our algorithms.

The code in the paper (a literate Prolog program, tested with SWI-Prolog and Lean Prolog) is available at http://logic.cse.unt.edu/tarau/research/2012/pcantor.pl.

Reseña: Logic + control: An example of program construction

PorJosé A. Alonso

Se ha publicado un trabajo sobre metodología de la programación en Prolog titulado Logic + control: An example of program construction.

Su autor es Wlodzimierz Drabent (de la Univ. de Linköping, Suecia).

El trabajo se presentará el 6 de Septiembre en el ICLP’12 (28th International Conference on Logic Programming).

Su resumen es

We present a Prolog program (the SAT solver of Howe and King) as a logic program with added control. The control consists of a selection rule (delays of Prolog) and pruning the search space. We construct the logic program together with proofs of its correctness and completeness, with respect to a formal specification. This is augmented by a proof of termination under any selection rule. Correctness and termination are inherited by the Prolog program, the change of selection rule preserves completeness. We prove that completeness is also preserved by one case of pruning; for the other an informal justification is presented.

For proving correctness we use a method, which should be well known but is often neglected. A contribution of this paper is a method for proving completeness. In particular we introduce a notion of semi-completeness, for which a local sufficient condition exists.

We compare the proof methods with declarative diagnosis (algorithmic debugging). We introduce a method of proving that a certain kind of pruning preserves completeness. We argue that the proof methods correspond to natural declarative thinking about programs, and that they can be used, formally or informally, in every-day programming.