Isabelle/HOL

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado Proof-by-instance for embedded network design.

Sus autores son

• Marc Boyer (de ONERA – The French Aerospace Lab, Toulouse, France),
• Loïc Fejoz (de RealTime-at-Work, Nancy, France) y
• Stephan Merz (Inria & LORIA, Nancy, France).

Su resumen es

Proof-by-instance is a technique that ensures the correctness of the results of a computation rather than proving correct the tool carrying out the computation. We report here on the application of this idea to check the computations relevant for analyzing time bounds for AFDX networks. We have demonstrated the feasibility of the approach by applying a proof-of-concept implementation to an AFDX network of realistic size, and we outline the roadmap towards a mature industrial toolset. This approach should lead to a reduction of the time and cost of developing analysis tools used in the design of embedded networks where certification is mandatory.

El trabajo se presentó el 6 de febrero en el ERTS² 2014 Embedded Real Time Software And Systems.

Se ha publicado un artículo automatización del razonamiento en Isabelle/HOL titulado A survey of axiom selection as a machine learning problem.

Sus autores son

• Daniel Kühlwein (de la Univ. de Nimega, Países Bajos). y
• Jasmin Christian Blanchette (de la Univ. Técnica de Munich, Alemania).

Su resumen es

Automatic theorem provers struggle to discharge proof obligations of interactive theorem provers. This is partly due to the large number of background facts that are passed to the automatic provers as axioms. Axiom selection algorithms predict the relevance of facts, thereby helping to reduce the search space of automatic provers. This paper presents an introduction to axiom selection as a machine learning problem and describes the challenges that distinguish it from other applications of machine learning.

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