Reseña

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre probabilidad titulado A formally verified proof of the central limit theorem

Sus autores son

• Jeremy Avigad (de la Carnegie Mellon University),
• Johannes Hölzl (del grupo Logic and Verification de la TU München) y
• Luke Serafin (de la Carnegie Mellon University).

Su resumen es

We describe a proof of the Central Limit Theorem that has been formally verified in the Isabelle proof assistant. Our formalization builds upon and extends Isabelle’s libraries for analysis and measure-theoretic probability. The proof of the theorem uses characteristic functions, which are a kind of Fourier transform, to demonstrate that, under suitable hypotheses, sums of random variables converge weakly to the standard normal distribution. We also discuss the libraries and infrastructure that supported the formalization, and reflect on some of the lessons we have learned from the effort.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí dentro del desarrollo de la teoría de la probabilidad.

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Refinement based verification of imperative data structures

Su autor es Peter Lammich (de la Chair for Logic and Verification en la Univ. técnica de Munich).

Su resumen es

In this paper we present a stepwise refinement based top-down approach to verified imperative data structures. Our approach is modular in the sense that already verified data structures can be used for construction of more complex data structures. Moreover, our data structures can be used as building blocks for the verification of algorithms. Our tool chain supports refinement down to executable code in various programming languages, and is fully implemented in Isabelle/HOL, such that its trusted code base is only the inference kernel and the code generator of Isabelle/HOL.

As a case study, we verify an indexed heap data structure, and use it to generate an efficient verified implementation of Dijkstra’s algorithm.

El trabajo se ha presentado en el CPP 2016 (The 5th ACM SIGPLAN Conference on Certified Programs and Proofs).

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

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Perron-Frobenius theorem for spectral radius analysis

Sus autores son

• Jose Divasón (del grupo PSYCOTRIP (Programming and Symbolic Computation Team of the University of La Rioja, España),
• Ondřej Kunčar (de la Chair for Logic and Verification en la Technische Universität München, Alemania),
• René Thiemann (del Computational Logic Group en la University of Innsbruck, Austria) y
• Akihisa Yamada (del Computational Logic Group en la University of Innsbruck, Austria).

Su resumen es

The spectral radius of a matrix A is the maximum norm of all eigenvalues of A. In previous work we already formalized that for a complex matrix A, the values in grow polynomially in n if and only if the spectral radius is at most one. One problem with the above characterization is the determination of all complex eigenvalues. In case A contains only non-negative real values, a simplification is possible with the help of the Perron-Frobenius theorem, which tells us that it suffices to consider only the real eigenvalues of A, i.e., applying Sturm’s method can decide the polynomial growth of A^n.

We formalize the Perron-Frobenius theorem based on a proof via Brouwer’s fixpoint theorem, which is available in the HOL multivariate analysis (HMA) library. Since the results on the spectral radius is based on matrices in the Jordan normal form (JNF) library, we further develop a connection which allows us to easily transfer theorems between HMA and JNF. With this connection we derive the combined result: if A is a non-negative real matrix, and no real eigenvalue of A is strictly larger than one, then An is polynomially bounded in n.

El trabajo se ha publicado en The Archive of Formal Proofs.

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