Reseña: Formalized timed automata

Buenos días

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Formalized timed automata.

Su autor es [Simon Wimmer] (de la Technische Universität München)

Su resumen es

Timed automata are a widely used formalism for modeling real-time systems, which is employed in a class of successful model check- ers such as UPPAAL. These tools can be understood as trust-multipliers: we trust their correctness to deduce trust in the safety of systems checked by these tools. However, mistakes have previously been made. This par- ticularly regards an approximation operation, which is used by model- checking algorithms to obtain a finite search space. The use of this op- eration left a soundness problem in the tools employing it, which was only discovered years after the first model checkers were devised. This work aims to provide certainty to our knowledge of the basic theory via formalization in Isabelle/HOL: we define the main concepts, formalize the classic decidability result for the language emptiness problem, prove correctness of the basic forward analysis operations, and finally outline how both streams of work can be combined to show that forward analysis with the common approximation operation correctly decides emptiness for the class of diagonal-free timed automata.

El trabajo se presentará en el ITP 2016: Interactive Theorem Proving

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

Reseña: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL.

Sus autores son Jesús Aransay y Jose Divasón (del grupo PSYCOTRIP (Programming and Symbolic Computation Team en la Universidad de la Rioja)

Su resumen es

In this contribution we present a formalised algorithm in the Isabelle/HOL proof assistant to compute echelon forms, and, as a consequence, characteristic polynomials of matrices. We have proved its correctness over Bézout domains, but its executability is only guaranteed over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This is possible since the algorithm has been parameterised by a (possibly non-computable) operation that returns the Bézout coefficients of a pair of elements of a ring. The echelon form is also used to compute determinants and inverses of matrices. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains, etc.). In order to improve performance, the algorithm has been refined to immutable arrays inside of Isabelle and code can be generated to functional languages as well.

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

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.

Reseña: Verification of an LCF-style first-order prover with equality

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado Verification of an LCF-style first-order prover with equality.

Sus autores son Alexander Birch Jensen, Anders Schlichtkrull y Jørgen Villadsen (del grupo Algorithms, logic and graphs en la Technical University of Denmark (DTU))

Su resumen es

We formalize in Isabelle/HOL the kernel of an LCF-style prover for first-order logic with equality from John Harrison’s Handbook of Practical Logic and Automated Reasoning. We prove the kernel sound and generate Standard ML code from the formalization. The generated code can then serve as a verified kernel. By doing this we also obtain verified components such as derived rules, a tableau prover, tactics, and a small declarative interactive theorem prover. We test that the kernel and the components give the same results as Harrison’s original on all the examples from his book. The formalization is 600 lines and is available online.

El trabajo se presentará en el Isabelle Workshop 2016.

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

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.

Libro de exámenes de programación funcional con Haskell (versión del 28 de julio de 2016)

He actualizado el libro Exámenes de programación funcional con Haskell. El libro es una recopilación de los exámenes de la asignatura de Informática (de primero del Grado en Matemáticas) desde el 2009-10 al actual.

Tras la ampliación, el libro contiene 155 exámenes con 1.012 ejercicios.

Este libro es el complemento de los anteriores:

Los códigos del libro están disponibles en Github https://github.com/jaalonso/Examenes_de_PF_con_Haskell.

Reseña: A formally verified proof of the central limit theorem

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

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.