Menu Close

Etiqueta: Reseña

Reseña: A framework for verifying depth-first search algorithms in Isabelle/HOL

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.

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.

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.

Reseña: Refinement based verification of imperative data structures

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

Reseña: Compass-free navigation of mazes

Se ha publicado un artículo de razonamiento formalizado en HOL Light sobre geometría titulado Compass-free navigation of mazes

Sus autores son Phil Scott y Jacques Fleuriot (de la Universidad de Edimburgo).

Su resumen es

If you find yourself in a corridor of a standard maze, a sure and easy way to escape is to simply pick the left (or right) wall, and then follow it along its twists and turns and around the dead-ends till you eventually arrive at the exit. But what happens when you cannot tell left from right? What if you cannot tell North from South? What if you cannot judge distances, and have no idea what it means to follow a wall in a given direction? The possibility of escape in these circumstances is suggested in the statement of an unproven theorem given in David Hilbert’s celebrated Foundations of Geometry, in which he effectively claimed that a standard maze could be fully navigated using axioms and concepts based solely on the relations of points lying on lines in a specified order. We discuss our algorithm for this surprisingly challenging version of the maze navigation problem, and our HOL Light verification of its correctness from Hilbert’s axioms.

El trabajo se ha presentado en el SCSS 2016 (7th International Symposium on Symbolic Computation in Software Science).

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

Reseña: Flag-based big-step semantics

Se ha publicado un artículo de razonamiento formalizado en Coq sobre semántica de lenguajes de programación titulado Flag-based big-step semantics.

Sus autores son

Su resumen es

Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules and premises for representing divergence than previous approaches in the literature.

El trabajo se ha desarrollado en el proyecto PLanCompS (Programming Language Components and Specifications).

El código de las correspondientes teorías en Coq 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: Perron-Frobenius theorem for spectral radius analysis

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

Sus autores son

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 A^n 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í.

Reseña: Software component design with the B method: a formalization in Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Software component design with the B method: a formalization in Isabelle/HOL.

Sus autores son

  • David Déharbe (del grupo ForAll (Formal Methods and Languages Laboratory) en la UFRN (Universidade Federal do Rio Grande do Norte), Brasil) y
  • Stephan Merz (del grupo VeriDis (Verification of Distributed Systems) en el INRIA Nancy & LORIA, Francia).

Su resumen es

This paper presents a formal development of an Isabelle/HOL theory for the behavioral aspects of artifacts produced in the design of software components with the B method. We first provide a formalization of semantic objects such as labelled transition systems and notions of behavior and simulation. We define an interpretation of the B method using such concepts. We also address the issue of component composition in the B method.

El trabajo se ha presentado en FACS 2015 (12th Intl. Conf. Formal Aspects of Component Software).

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.