Meses: agosto 2016

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Proving divide and conquer complexities in Isabelle/HOL

Su autor es Manuel Eberl (de la Technische Universität München, Alemania).

Su resumen es

The Akra–Bazzi method, a generalisation of the well-known Master Theorem, is a useful tool for analysing the complexity of Divide & Conquer algorithms. This work describes a formalisation of the Akra–Bazzi method (as generalised by Leighton) in the interactive theorem prover Isabelle/HOL and the derivation of a generalised version of the Master Theorem from it. We also provide some automated proof methods that facilitate the application of this Master Theorem and allow mostly automatic verification of Θ-bounds for these Divide & Conquer recurrences. To our knowledge, this is the first formalisation of theorems for the analysis of such recurrences.

La versión final del trabajo se ha publicado en el Journal of Automated Reasoning.

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 sobre álgebra titulado A decision procedure for univariate real polynomials in Isabelle/HOL.

Su autor es Manuel Eberl (de la Technische Universität München, Alemania).

Su resumen es

Sturm sequences are a method for computing the number of real roots of a univariate real polynomial inside a given interval efficiently. In this paper, this fact and a number of methods to construct Sturm sequences efficiently have been formalised with the interactive theorem prover Isabelle/HOL. Building upon this, an Isabelle/HOL proof method was then implemented to prove interesting statements about the number of real roots of a univariate real polynomial and related properties such as non-negativity and monotonicity.

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

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