Executable Multivariate Polynomials

PorJosé A. Alonso

Christian Sternagel y René Thiemann han publicado en The Archive of Formal Proofs el artículo Executable Multivariate Polynomials.

El artículo es parte del proyecto IsaFoR/CeTA (Isabelle Formalization of Rewriting / Certified Termination Analysis) cuyo objetivo es la formalización en Isabelle de técnicas de terminación. Los ficheros del proyecto se encuentran aquí.

Una de las técnicas usadas para demostrar la terminación de sistemas de reescritura se basa en las interpretaciones polinómicas.

En el artículo Executable Multivariate Polynomials se presenta una formalización en Isabelle de los polinomios con varias variables con coeficientes en un semianillo ordenado. Se definen las operaciones de polinomios (suma, multiplicación y sustitución) y la ordenación de polinomios. La formalización también incluye el criterio de Neurauter, Zankl y Middeldorp monotocidad de interpretaciones polinómicas sobre los naturales.

Formal Power Series

PorJosé A. Alonso

Acaba de publicarse un nuevo artículo de razonamiento formalizado. El artículo es Formal Power Series publicado por Amine Chaieb en el Journal of Automated Reasoning.

El resumen que hace el autor del artículo es el siguiente: We present a formalization of the topological ring of formal power series in Isabelle/HOL. We also formalize formal derivatives, division, radicals, composition and reverses. As an application, we show how formal elementary and hyper-geometric series yield elegant proofs for some combinatorial identities. We easily derive a basic theory of polynomials. Then, using a generic formalization of the fraction field of an integral domain, we obtain formal Laurent series and rational functions for free.

La formalización completa se encuentra en Theory Formal Power Series

Razonamiento formalizado en análisis numérico

PorJosé A. Alonso

Hoy se ha publicado en arXiv el artículo Formal Proof of a Wave Equation Resolution Scheme: the Method Error escrito por Sylvie Boldo (INRIA Saclay – Ile de France, LRI), Francois Clement (INRIA Rocquencourt), Jean-Christophe Filliâtre (INRIA Saclay – Ile de France, LRI), Micaela Mayero (LIPN, INRIA Rhône-Alpes / LIP Laboratoire de l’Informatique du Parallélisme), Guillaume Melquiond (INRIA Saclay – Ile de France, LRI) y Pierre Weis (INRIA Rocquencourt).

En este trabajo se presenta una formalización en Coq de una parte del conocimiento matemático más usado en las ingeniería: las ecuaciones diferenciales. Curiosamente las ecuaciones diferenciales apenas se han tratado dentro del razonamiento formalizado.

Read More “Razonamiento formalizado en análisis numérico”

Métodos formales y seguridad en la Red

PorJosé A. Alonso

Hoy publica “El País” el artículo España, blanco de más de cuarenta ciberataques. El artículo es un reportaje sobre “la guerra de los ciberespías” a raíz del ataque a Google. Además cuenta las iniciativas españolas para aumentar la seguridad.

Desde sus inicios los métodos formales se han aplicado a aumentar la seguridad de los sistemas críticos y, más generalmente, a la ingeniería de la seguridad. Dado el uso de la Red, sus programas y servicios se están convirtiendo en sistemas críticos y, por tanto, en campo de aplicación de los métodos formales. Muestra del interés de los sistemas de Red para los métodos formales son la realización de tesis como las siguientes
Read More “Métodos formales y seguridad en la Red”