Reseña: Echelon form in Isabelle/HOL

PorJosé A. Alonso

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

Reseña: Isabelle and security

PorJosé A. Alonso

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

Sus autores son

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.

Reseña: Machine-checked proofs for realizability checking algorithms

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre titulado Machine-checked proofs for realizability checking algorithms.

Sus autores son

Su resumen es

We have recently proposed a contract-based realizability checking algorithm involving the use of theories, to provide an auxiliary procedure to consistency checking of “leaf-level” components in complex embedded systems. To prove the soundness of our approach on realizability, we formalized the necessary definitions and theorems of Towards realizability checking of contracts using theories, in the Coq proof and specification language.

El código de las correspondientes teorías en Coq se encuentra [aquí](.https://github.com/andrewkatis/Coq/
blob/master/realizability/Realizability.v).

Reseña: Verifying fast and sparse SSA-based optimizations in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre
compiladores titulado Verifying fast and sparse SSA-based optimizations in Coq .

Sus autores son Delphine Demange, David Pichardie y Léo Stefanesco (del grupo Celtique en el INRIA Rennes, Francia).

Su resumen es

The Static Single Assignment (SSA) form is a predominant technology in modern compilers, enabling powerful and fast program optimizations. Despite its great success in the implementation of pro- duction compilers, it is only very recently that this technique has been introduced in verified compilers. As of today, few evidence exist on that, in this context, it also allows faster and simpler optimizations. This work builds on the CompCertSSA verified compiler (an SSA branch of the verified CompCert C compiler). We implement and verify two prevail- ing SSA optimizations: Sparse Conditional Constant Propagation and Global Value Numbering. For both transformations, we mechanically prove their soundness in the Coq proof assistant. Both optimization proofs are embedded in a single sparse optimization framework, factoring out many of the dominance-based reasoning steps required in proofs of SSA-based optimizations. Our experimental evaluations indicate both a better precision, and a significant compilation time speedup.

El trabajo se presentará en CC 2015 (24th International Conference on Compiler Construction).

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

Reseña: Formal proofs for nonlinear optimization

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Formal proofs for nonlinear optimization.

Sus autores son

Su resumen es

We present a formally verified global optimization framework. Given a semialgebraic or transcendental function f and a compact semialgebraic domain K, we use the nonlinear maxplus template approximation algorithm to provide a certified lower bound of f over K.

This method allows to bound in a modular way some of the constituents of f by suprema of quadratic forms with a well chosen curvature. Thus, we reduce the initial goal to a hierarchy of semialgebraic optimization problems, solved by sums of squares relaxations.

Our implementation tool interleaves semialgebraic approximations with sums of squares witnesses to form certificates. It is interfaced with Coq and thus benefits from the trusted arithmetic available inside the proof assistant. This feature is used to produce, from the certificates, both valid underestimators and lower bounds for each approximated constituent.

The application range for such a tool is widespread; for instance Hales’ proof of Kepler’s conjecture yields thousands of multivariate transcendental inequalities. We illustrate the performance of our formal framework on some of these inequalities as well as on examples from the global optimization literature.

El trabajo se ha publicado en el Journal of Formalized Reasoning.

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