Reseña: Formal reasoning about finite-state discrete-time Markov chains in HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre procesos de Markov titulado Formal reasoning about finite-state discrete-time Markov chains in HOL.

Sus autores son Liya Liu, Osman Hasan y Sofiène Tahar (de la Univ. de Concordia, Canadá).

Su resumen es

Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.

La revista en donde que ha publicado el artículo es el Journal of Computer Science and Technology.

Reseña: Mechanising Turing machines and computability theory in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre modelos de computación titulado Mechanising Turing machines and computability theory in Isabelle/HOL.

Sus autores son Jian Xu, Xingyuan Zhang y Christian Urban.

Su resumen es

We present a formalised theory of computability in the theorem prover Isabelle/HOL. This theorem prover is based on classical logic which precludes direct reasoning about computability: every boolean predicate is either true or false because of the law of excluded middle. The only way to reason about computability in a classical theorem prover is to formalise a concrete model of computation. We formalise Turing machines and relate them to abacus machines and recursive functions. We also formalise a universal Turing machine and Hoare-style reasoning techniques that allow us to reason about Turing machine programs. Our theory can be used to formalise other computability results.

Las teorías desarrolladas en Isabelle/HOL se encuentran en aquí.

Reseña: The Picard algorithm for ordinary differential equations in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre ecuaciones diferenciales titulado The Picard algorithm for ordinary differential equations in Coq.

Sus autores son Evgeny Makarov and Bas Spitters (de la Universidad de Nimega, Países Bajos).

Su resumen es

Ordinary Differential Equations (ODEs) are ubiquitous in physical applications of mathematics. The Picard-Lindelöf theorem is the first fundamental theorem in the theory of ODEs. It allows one to solve differential equations numerically. We provide a constructive development of the Picard-Lindelöf theorem which includes a program together with sufficient conditions for its correctness. The proof/program is written in the Coq proof assistant and uses the implementation of efficient real numbers from the CoRN library and the MathClasses library. Our proof makes heavy use of operators and functionals, functions on spaces of functions. This is faithful to the usual mathematical description, but a novel level of abstraction for certified exact real computation.

Las teorías desarrolladas se encuentran aquí.

Reseña: Contributions to the formal verification of arithmetic algorithms

PorJosé A. Alonso

El pasado mes de septiembre se presentó una tesis sobre verificación formal con Coq titulada Contributions to the formal verification of arithmetic algorithms.

Su autor es Érik Martin-Dorel, dirigido por Micaela Mayero y Jean-Michel Muller.

Su resumen es

The Floating-Point (FP) implementation of a real-valued function is performed with correct rounding if the output is always equal to the rounding of the exact value, which has many advantages. But for implementing a function with correct rounding in a reliable and efficient manner, one has to solve the “Table Maker’s Dilemma” (TMD). Two sophisticated algorithms (L and SLZ) have been designed to solve this problem, relying on some long and complex calculations that are performed by some heavily-optimized implementations. Hence the motivation to provide strong guarantees on these costly pre-computations. To this end, we use the Coq proof assistant. First, we develop a library of “Rigorous Polynomial Approximation”, allowing one to compute an approximation polynomial and an interval that bounds the approximation error in Coq. This formalization is a key building block for verifying the first step of SLZ, as well as the implementation of a mathematical function in general (with or without correct rounding). Then we have implemented, formally verified and made effective 3 interrelated certificates checkers in Coq, whose correctness proof derives from Hensel’s lemma that we have formalized for both univariate and bivariate cases. In particular, our “ISValP verifier” is a key component for formally verifying the results generated by SLZ. Then, we have focused on the mathematical proof of “augmented-precision” FP algorithms for the square root and the Euclidean 2D norm. We give some tight lower bounds on the minimum non-zero distance between sqrt(x²+y²) and a midpoint, allowing one to solve the TMD for this bivariate function. Finally, the “double-rounding” phenomenon can typically occur when several FP precision are available, and may change the behavior of some usual small FP algorithms. We have formally verified in Coq a set of results describing the behavior of the Fast2Sum algorithm with double-roundings.

Las transparencias usadas en la presentación se encuentran aquí.

Reseña: The Boyer-Moore waterfall model revisited

PorJosé A. Alonso

Uno de los problemas fundamentales dentro del campo del razonamiento automático es la automatización de la inducción. El método fundamental para automatizar la inducción es el de la cascada presentado por Robert S. Boyer y J S. Moore en su libro A Computational Logic e integrado en sus sistemas Nqthm y ACL2.

En el trabajo The Boyer-Moore waterfall model revisited se presenta una implementación del modelo de Boyer-Moore en el sistema HOL Light.

Sus autores son Petros Papapanagiotou y Jacques Fleuriot (de la Universidad de Edimburgo).

Su resumen es

In this paper, we investigate the potential of the Boyer-Moore waterfall model for the automation of inductive proofs within a modern proof assistant. We analyze the basic concepts and methodology underlying this 30-year-old model and implement a new, fully integrated tool in the theorem prover HOL Light that can be invoked as a tactic. We also describe several extensions and enhancements to the model. These include the integration of existing HOL Light proof procedures and the addition of state-of-the-art generalization techniques into the waterfall. Various features, such as proof feedback and heuristics dealing with non-termination, that are needed to make this automated tool useful within our interactive setting are also discussed. Finally, we present a thorough evaluation of the approach using a set of 150 theorems, and discuss the effectiveness of our additions and relevance of the model in light of our results.

El trabajo es una extensión de la Tesis de Máster de Petros Papapanagiotou titulada On the automation of inductive proofs in HOL
Light y sirve como lectura complementaria en el curso Automated Reasoning (2012-13) de la Universidad de Edimburgo. Las transparencias del correspondiente tema del curso son Inductive theorem proving.