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

Reseña: Stream fusion for Isabelle’s code generator

PorJosé A. Alonso

Se ha publicado un artículo de automatización del razonamiento formalizado en Isabelle/HOL Stream fusion for Isabelle’s code generator.

Sus autores son Andreas Lochbihler y Alexandra Maximova (del Information Security Group en la Escuela Politécnica Federal de Zúrich, Suiza).

Su resumen es

Stream fusion eliminates intermediate lists in functional code. We formalise stream fusion for finite and coinductive lists in Isabelle/HOL and implement the transformation in the code preprocessor. Our initial results show that optimisations during code extraction can boost the performance of the generated code, but the transformation requires further engineering to be usable in practice.

Su contenido es un resumen de la tesis de Máster Stream Fusion for Isabelle’s Code Generator realizada por Alexandra Maximova y dirigida por Andreas Lochbihler.

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

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

Reseña: The Akra-Bazzi theorem and the Master theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado The Akra-Bazzi theorem and the Master theorem.

Su autor es Manuel Eberl (del Theorem Proving Group en la Technische Universität München, Munich, Alemania).

Su resumen es

This article contains a formalisation of the Akra-Bazzi method based on a proof by Leighton. It is a generalisation of the well-known Master Theorem for analysing the complexity of Divide & Conquer algorithms. We also include a generalised version of the Master theorem based on the Akra-Bazzi theorem, which is easier to apply than the Akra-Bazzi theorem itself.

Some proof methods that facilitate applying the Master theorem are also included. For a more detailed explanation of the formalisation and the proof methods, see the accompanying paper (publication forthcoming).

El trabajo se ha publicado en AFP (The Archive of Formal Proofs).

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

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático y Lógica computacional y teoría de modelos.

Reseña: Landau symbols en Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Landau symbols en Isabelle/HOL.

Sus autor es Manuel Eberl (del Theorem Proving Group en la Technische Universität München, Munich, Alemania).

Su resumen es

This entry provides Landau symbols to describe and reason about the asymptotic growth of functions for sufficiently large inputs. A number of simplification procedures are provided for additional convenience: cancelling of dominated terms in sums under a Landau symbol, cancelling of common factors in products, and a decision procedure for Landau expressions containing products of powers of functions like x, ln(x), ln(ln(x)) etc.

El trabajo se ha publicado en The Archive of Formal Proofs.

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

Este trabajo puede servir como lectura complementaria del curso de Razonamiento automático.

Reseña: MathCheck: A math assistant via a combination of computer algebra systems and SAT solvers

PorJosé A. Alonso

Se ha publicado un artículo de aplicación del razonamiento automático en la enseñanza titulado MathCheck: A math assistant via a combination of computer algebra systems and SAT solvers.

Sus autores son
+ Edward Zulkoski (del GSD Lab (Generative software development lab))
+ Vijay Ganesh (del Waterloo computer-aided reasoning group) y
+ Krzysztof Czarnecki (del GSD Lab (Generative software development lab))

de la Univ. de Waterloo, Ontario, Canadá.

Su resumen es

We present a method and an associated system, called Math-Check, that embeds the functionality of a computer algebra system (CAS) within the inner loop of a conflict-driven clause-learning SAT solver. SAT+CAS systems, a la MathCheck, can be used as an assistant by mathematicians to either counterexample or finitely verify open universal conjectures on any mathematical topic (e.g., graph and number theory, algebra, geometry, etc.) supported by the underlying CAS system. Such a SAT+CAS system combines the efficient search routines of modern SAT solvers, with the expressive power of CAS, thus complementing both. The key insight behind the power of the SAT+CAS combination is that the CAS system can help cut down the search-space of the SAT solver, by providing learned clauses that encode theory-specific lemmas, as it searches for a counterexample to the input conjecture (just like the T in DPLL(T)). In addition, the combination enables a more efficient encoding of problems than a pure Boolean representation.

In this paper, we leverage the graph-theoretic capabilities of an open-source CAS, called SAGE. As case studies, we look at two long-standing open mathematical conjectures from graph theory regarding properties of hypercubes: the first conjecture states that any matching of any d-dimensional hypercube can be extended to a Hamiltonian cycle; and the second states that given an edge-antipodal coloring of a hypercube, there always exists a monochromatic path between two antipodal vertices. Previous results have shown the conjectures true up to certain low-dimensional hypercubes, and attempts to extend them have failed until now. Using our SAT+CAS system, MathCheck, we extend these two conjectures to higher-dimensional hypercubes. We provide detailed performance analysis and show an exponential reduction in search space via the SAT+CAS combination relative to finite brute-force search.

El trabajo se ha presentado en el CADE-25 (The 25th International Conference on Automated Deduction).

El sistema MatCheck se encuentra aquí y su código aquí.