Reseña

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre grafos titulado Properties of random graphs – subgraph containment.

Sus autor es Lars Hupel (de la Univ. Politécnica de Munich).

Su resumen es

Random graphs have been introduced by Erdös and Rényi in [1]. They describe a probability space where, for a fixed number of vertices, each possible edge is present with a certain probability independent from other edges, but with the same probability for each edge. They study what properties emerge when increasing the number of vertices, or as they call it, “the evolution of such a random graph”. The theorem which we will prove here is a slightly different version from that in the first section of that paper.

Here, we are interested in the probability that a random graph contains a certain pattern, for example a cycle or a clique. A very high edge probability gives rise to perhaps too many edges, which is usually undesired since it degrades the performance of many algorithms, whereas a low edge probability might result in a disconnected graph. The central theorem determines a threshold probability such that a higher edge probability will asymptotically almost surely produce a random graph with the desired subgraph.

The proof is outlined in [2, §11.4] and [3, §3]. The work is based on the comprehensive formalization of probability theory in Isabelle/HOL and on a previous definition of graphs in a work by Noschinski [4]. There, Noschinski formalized the proof that graphs with arbitrarily large girth and chromatic number exist. While the proof in this paper uses a different approach, the definition of a probability space on edges turned out to be quite useful.

El trabajo se ha publicado en Archive of Formal Proofs

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

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado Verifying document confidentiality of a conference management system.

Sus autores son Sudeep Kanav, Peter Lammich y Andrei Popescu (de la Universidad Técnica de Munich).

Su resumen es

We present a case study in verified security for realistic systems: the implementation of a conference management system, whose functional kernel is faithfully represented in the Isabelle theorem prover, where we specify and verify confidentiality properties. The various theoretical and practical challenges posed by this development led to some novel security model and verification method that we hope is reusable for other multi-user document management systems.

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado Applications of the Gauss-Jordan algorithm, done right.

Sus autores son Jesús María Aransay y José Divasón (de la Univ. de la Rioja).

Su resumen es

Computer Algebra systems are widely spread because of some of their remarkable features such as their ease of use and performance. Nonetheless, this focus on performance sometimes leads to unwanted consequences: algorithms and computations are implemented and carried out in a way which is sometimes not transparent to the users, and that can lead to unexpected failures.

In this paper we present a formalisation in a proof assistant system of a naive version of the Gauss-Jordan algorithm, with explicit proofs of some of its applications, and additionally a process to obtain versions of this algorithm in two different functional languages (SML and Haskell) by means of code generation techniques from the verified algorithm. The obtained programs are then applied to test cases, which, despite the simplicity of the original algorithm, have shown remarkable features in comparison to some Computer Algebra systems, such as Mathematica (where some of these computations are even incorrect), or Sage (in comparison to which the generated programs show a compelling performance).

The aim of the paper is to show that, with the current technology in Theorem Proving, formalising Linear Algebra procedures is a challenging but rewarding task, which provides programs that can be compared in some aspects to state of the art procedures in Computer Algebra systems, and whose correctness is formally proved.

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