Coq

Se ha publicado un artículo de razonamiento formalizado en Coq sobre la aritmética titulado Formal verification of programs computing the floating-point average.

Sus autora es Silvie Boldo (del grupo Toccata (Formally Verified Programs, Certified Tools and Numerical Computations) en el LRI (Laboratoire de Recherche en Informatique) de la Universidad Paris-Sur).

Su resumen es

The most well-known feature of floating-point arithmetic is the limited precision, which creates round-off errors and inaccuracies. Another important issue is the limited range, which creates underflow and overflow, even if this topic is dismissed most of the time. This article shows a very simple example: the average of two floating-point numbers. As we want to take exceptional behaviors into account, we cannot use the naive formula (x+y)/2. Based on hints given by Sterbenz, we first write an accurate program and formally prove its properties. An interesting fact is that Sterbenz did not give this program, but only specified it. We prove this specification and include a new property: a precise certified error bound. We also present and formally prove a new algorithm that computes the correct rounding of the average of two floating-point numbers. It is more accurate than the previous one and is correct whatever the inputs.

El trabajo se presentará en el ICFEM 2015 (The 17th International Conference on Formal Engineering Methods).

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

Se ha publicado un artículo de razonamiento formalizado en Coq sobre geometría titulado A synthetic proof of Pappus’ theorem in Tarski’s geometry

Sus autores son Gabriel Braun y Julien Narboux (del Équipe Informatique Géométrique et Graphique en la Universidad de Estrasburgo, Francia).

Su resumen es

In this paper, we report on the formalization of a synthetic proof of Pappus’ theorem. We provide two versions of the theorem: the first one is proved in neutral geometry (without assuming the parallel postulate), the second (usual) version is proved in Euclidean geometry. The proof that we formalize is the one presented by Hilbert in The Foundations of Geometry which has been detailed by Schwabhäuser, Szmielew and Tarski in part I of Metamathematische Methoden in der Geometrie. We highlight the steps which are still missing in this later version. The proofs are checked formally using the Coq proof assistant. Our proofs are based on Tarski’s axiom system for geometry without any continuity axiom. This theorem is an important milestone toward obtaining the arithmetization of geometry which will allow us to provide a connection between analytic and synthetic geometry.

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

Se ha publicado un artículo de razonamiento formalizado en Coq sobre geometría titulado Parallel postulates and decidability of intersection of lines: a mechanized study within Tarski’s system of geometry.

Sus autores son Pierre Boutry, Julien Narboux y Pascal Schreck (del Équipe Informatique Géométrique et Graphique en la Universidad de Estrasburgo, Francia)

Su resumen es

In this paper we focus on the formalization of the proof of equivalence between different versions of Euclid’s 5 th postulate. This postulate is of historical importance because for centuries many mathematicians believed that this statement was rather a theorem which could be derived from the first four of Euclid’s postulates and history is rich of incorrect proofs of Euclid’s 5 th postulate. These proofs are incorrect because they assume more or less implicitly a statement which is equivalent to Euclid’s 5 th postulate and whose validity is taken for granted. Even though these proofs are incorrect the attempt was not pointless because the flawed proof can be turned into a proof that the unjustified statement implies the parallel postulate. In this paper we provide formal proofs verified using the Coq proof assistant that 10 different statements are equivalent to Euclid’s 5 th postulate. We work in the context of Tarski’s neutral geometry without continuity nor Archimedes’ axiom. The formalization provide a clarification of the hypotheses used for the proofs. Following Beeson, we study the impact of the choice of a particular version of the parallel postulate on the decidability issues.

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

Se ha publicado un artículo de razonamiento formalizado en Coq sobre topología algebraica titulado A formal verification of the theory of parity complexes.

Su autor es Mitchell Buckley (de la Macquarie University en Australia).

Su resumen es

We formalise, in Coq, the opening sections of Parity Complexes up to and including the all important excision of extremals algorithm. Parity complexes describe the essential combinatorial structure exhibited by simplexes, cubes and globes, that enable the construction of free ω-categories on such objects. The excision of extremals is a recursive algorithm that presents every cell in such a category as a composite of atomic cells, this is the sense in which the ω-category is free. Due to the complicated multi-dimensional nature of this work, the detail of definitions and proofs can be hard to follow and verify. Indeed, some corrections [Street1994] were required some years following the original publication. Our formalisation verifies that all cases of each result operate as stated. In particular, we indicate which portions of the theory can be proved directly from definitions, and which require more subtle and complex arguments. By identifying results that require the most complicated proofs, we are able to investigate where this theory might benefit from further study and which results need to be considered most carefully in future work.

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

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Program verification by coinduction.

Sus autores son Brandon Moore y Grigore Rosu (del Formal Systems Laboratory en la Universidad de Illinois en Urbana-Champaign).

Su resumen es

We present a program verification framework based on coinduction, which makes it feasible to verify programs directly against an operational semantics, without requiring intermediates like axiomatic semantics or verification condition generators. Specifications can be written and proved using any predicates on the state space of the operational semantics.

We implement our approach in Coq, giving a certifying language-independent verification framework. The core proof system is implemented as a single module imported unchanged into proofs of programs in any semantics. A comfortable level of automation is provided by instantiating a simple heuristic with tactics for language-specific tasks such as finding the successor of a symbolic state, and for domain-specific reasoning about the predicates used in a particular specification. This approach also smoothly allows manual assistance at points the automation cannot handle.

We demonstrate the power of our approach by verifying algorithms as complicated as Schorr-Waite graph marking, and the versatility by instantiating it for object languages in several styles of semantics. Despite the greater flexibility and generality of our approach, proof size and proof/certificate-checking time compare favorably with Bedrock, another Coq-based certifying program verification framework.