Reseña: A formalisation of finite automata using hereditarily finite sets

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre teoría de conjuntos titulado A formalisation of finite automata using hereditarily finite sets

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

Hereditarily finite (HF) set theory provides a standard universe of sets, but with no infinite sets. Its utility is demonstrated through a formalisation of the theory of regular languages and finite automata, including the Myhill-Nerode theorem and Brzozowski’s minimisation algorithm. The states of an automaton are HF sets, possibly constructed by product, sum, powerset and similar operations.

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

I1M2014: División y factorización de polinomios mediante la regla de Ruffini

PorJosé A. Alonso

En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la relación 18. El objetivo de la relación es implementar la regla de Ruffini y sus aplicaciones utilizando las implementaciones del TAD de polinomio estudiadas en el tema 21.

En los ejercicios se usan las siguientes librerías:

  • PolRepTDA: Implementación de los polinomios mediante tipos de datos algebraicos.
  • PolRepDispersa: Implementación de los polinomios mediante listas dispersas.
  • PolRepDensa: Implementación de los polinomios mediante listas densas.
  • PolOperaciones: Operaciones con el TAD de los polinomios.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2014: División y factorización de polinomios mediante la regla de Ruffini”

Reseña: Program verification by coinduction

PorJosé A. Alonso

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.