Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre teoría de conjuntos titulado A formalisation of finite automata using hereditarily finite sets

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

Hereditarily finite (HF) set theory provides a standard universe of sets, but with no infinite sets. Its utility is demonstrated through a formalisation of the theory of regular languages and finite automata, including the Myhill-Nerode theorem and Brzozowski’s minimisation algorithm. The states of an automaton are HF sets, possibly constructed by product, sum, powerset and similar operations.

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

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado QR decomposition.

Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).

Su resumen es

QR decomposition is an algorithm to decompose a real matrix A into the product of two other matrices Q and R, where Q is orthogonal and R is invertible and upper triangular. The algorithm is useful for the least squares problem; i.e., the computation of the best approximation of an unsolvable system of linear equations. As a side-product, the Gram-Schmidt process has also been formalized. A refinement using immutable arrays is presented as well. The development relies, among others, on the AFP entry Implementing field extensions of the form Q{sqrt(b)}” by René Thiemann, which allows execution of the algorithm using symbolic computations. Verified code can be generated and executed using floats as well.

El trabajo se ha publicado la semana pasada en The Archive of Formal Proofs

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

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado Echelon form.

Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).

Su resumen es

We formalize an algorithm to compute the Echelon Form of a matrix. We have proved its existence over Bézout domains and made it executable over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This allows us to compute determinants, inverses and characteristic polynomials of matrices. The work is based on the HOL-Multivariate Analysis library, and on both the Gauss-Jordan and Cayley-Hamilton AFP entries. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains, …). The algorithm has been refined to immutable arrays and code can be generated to functional languages as well.

El trabajo se ha publicado la semana pasada en The Archive of Formal Proofs

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

Se ha publicado un artículo sobre verifiación formal con Isabelle/HOL titulado Isabelle and security

Sus autores son

• Jasmin Christian Blanchette (del grupo VeriDis (Verification of Distributed Systems) en el Inria Nancy & LORIA y del grupo Automation of Logic en el Max Planck Institute for Informatics de Saarbrücken) y
• Andrei Popescu (del grupo Foundations of Computing en la Middlesex University London).

Su resumen es

Isabelle/HOL is a general-purpose proof assistant based on higher-order logic. Its main strengths are its simple-yet-expressive logic and its proof automation. Security researchers make up a significant fraction of Isabelle’s users. In the past few years, many exciting developments have taken place, connecting programming languages, operating system kernels, and security.