Reseña

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Relation-algebraic verification of Prim’s minimum spanning tree algorithm.

Su autor es Walter Guttmann (de la University of Canterbury, Nueva Zelanda).

Su resumen es

We formally prove the correctness of Prim’s algorithm for computing minimum spanning trees. We introduce new generalisations of relation algebras and Kleene algebras, in which most of the proof can be carried out. Only a small part needs additional operations, for which we introduce a new algebraic structure. We instantiate these algebras by matrices over extended reals, which model the weighted graphs used in the algorithm. Many existing results from relation algebras and Kleene algebras generalise from the relation model to the weighted-graph model with no or small changes. The overall structure of the proof uses Hoare logic. All results are formally verified in Isabelle/HOL heavily using its integrated automated theorem provers.

El trabajo se presentará el 24 de octubre en el ICTAC2016 (13th International Colloquium on Theoretical Aspects of Computing).

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 sobre algorítmica titulado A framework for verifying depth-first search algorithms in Isabelle/HOL.

Sus autores son Peter Lammich y René Neumann (de la Technische Universität München)

Su resumen es

Many graph algorithms are based on depth-first search (DFS).The formalizations of such algorithms typically share many common ideas. In this paper, we summarize these ideas into a framework in Isabelle/HOL.

Building on the Isabelle Refinement Framework, we provide support for a refinement based development of DFS based algorithms, from phrasing and proving correct the abstract algorithm, over choosing an adequate implementation style (e. g., recursive, tail-recursive), to creating an executable algorithm that uses efficient data structures.

As a case study, we verify DFS based algorithms of different complexity, from a simple cyclicity checker, over a safety property model checker, to complex algorithms like nested DFS and Tarjan’s SCC algorithm.

El trabajo se ha presentado en The 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015)

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.

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í.

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.

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.