Reseña: Windmills of the minds: an algorithm for Fermat’s two squares theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre teoría de números titulado Windmills of the minds: an algorithm for Fermat’s two squares theorem.

Sus autor es Hing Lun Chan (de la Australian National University en Canberra, Australia).

Su resumen es

The two squares theorem of Fermat is a gem in number theory, with a spectacular one-sentence “proof from the Book“. Here is a formalisation of this proof, with an interpretation using windmill patterns. The theory behind involves involutions on a finite set, especially the parity of the number of fixed points in the involutions. Starting as an existence proof that is non-constructive, there is an ingenious way to turn it into a constructive one. This gives an algorithm to compute the two squares by iterating the two involutions alternatively from a known fixed point.

El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.

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

Reseña: Verified over-approximation of the diameter of propositionally factored transition systems

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre verificación titulado Verified over-approximation of the diameter of propositionally factored transition systems.

Sus autores son
+ Mohammad Abdulaziz (del Software Systems Research Group del NICTA en Camberra, Australia),
+ Charles Gretton (de la Australian National University en Camberra, Australia) y
+ Michael Norrish (del Software Systems Research Group del NICTA en Camberra, Australia)

Su resumen es

To guarantee the completeness of bounded model checking (BMC) we require a completeness threshold. The diameter of the Kripke model of the transition system is a valid completeness threshold for BMC of safety properties. The recurrence diameter gives us an upper bound on the diameter for use in practice. Transition systems are usually described using (propositionally) factored representations. Bounds for such lifted representations are calculated in a compositional way, by first identifying and bounding atomic subsystems, and then composing those results according to subsystem dependencies to arrive at a bound for the concrete system. Compositional approaches are invalid when using the diameter to bound atomic subsystems, and valid when using the recurrence diameter. We provide a novel overapproximation of the diameter, called the sublist diameter, that is tighter than the recurrence diameter. We prove that compositional approaches are valid using it to bound atomic subsystems. Those proofs are mechanised in HOL4. We also describe a novel verified compositional bounding technique which provides tighter overall bounds compared to existing bottom-up approaches.

El trabajo se presentó el 26 de agosto en el ITP 2015 (The 6th conference on Interactive Theorem Proving).

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

Steps towards verified implementations of HOL Light

PorJosé A. Alonso

Una de la líneas de trabajo dentro de la automatización del razonamiento es la verificación de sistemas de razonamiento. En dicha línea se ha publicado un trabajo titulado Steps towards verified implementations of HOL Light.

Sus autores son

Su resumen es

This short paper describes our plans and progress towards construction of verified ML implementations of HOL Light: the first formally proved soundness result for an LCF-style prover. Building on Harrison’s formalisation of the HOL Light logic and our previous work on proof-producing synthesis of ML, we have produced verified implementations of each of HOL Light’s kernel functions. What remains is extending Harrison’s soundness proof and proving that ML’s module system provides the required abstraction for soundness of the kernel to relate to the entire theorem prover. The proofs described in this paper involve the HOL Light and HOL4 theorem provers and the OpenTheory toolchain.

El trabajo se presentó en el ITP 2013 (4th Conference on Interactive Theorem Proving).

Proof pearl: A verified bignum implementation in x86-64 machine code

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en HOL4 titulado Proof pearl: A verified bignum implementation in x86-64 machine code.

Sus autores son

  • Magnus O. Myreen (de la Universidad de Cambridge)y
  • Gregorio Curello (de la Universidad Autónoma de Barcelona).

Su resumen es

Verification of machine code can easily deteriorate into an endless clutter of low-level details. This paper presents a case study which shows that machine-code verification does not necessarily require ghastly low-level proofs. The case study we describe is the construction of an x86-64 implementation of arbitrary-precision integer arithmetic. Compared with closely related work, our proofs are shorter and, more importantly, the reasoning is at a more convenient high level of abstraction, e.g. pointer reasoning is largely avoided. We achieve this improvement as a result of using previously developed tools, namely, a proof-producing decompiler and compiler. The work presented in this paper has been developed in the HOL4 theorem prover and the case study resulted in 700 lines of verified 64-bit x86 machine code.

El código correspondiente se encuentra aquí.

El trabajo se presentará en la CPP 2013 (3rd International Conference on Certified Programs and Proofs).

Reseña: “Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁”

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre teoría de conjuntos titulado Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁.

Sus autores son Michael Norrish (del (Canberra Research Lab., NICTA) y Brian Huffman (de Galois, Inc.).

El trabajo se ha presentado esta semana en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

We describe a comprehensive HOL mechanisation of the theory of ordinal numbers, focusing on the basic arithmetic operations. Mechanised results include the existence of fixpoints such as ε₀ , the existence of normalforms, and the validation of algorithms used in the ACL2 theorem-proving system.

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