Reseña: Formalization of incremental simplex algorithm by stepwise refinement

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Formalization of incremental simplex algorithm by stepwise refinement.

Sus autores son Mirko Spasić and Filip Marić (de la Universidad de Belgrado).

Su resumen es

We present an Isabelle/HOL formalization and total correctness proof for the incremental version of the Simplex algorithm which is used in most state-of-the-art SMT solvers. Formalization relies on stepwise program and data refinement, starting from a simple specification, going through a number of fine refinement steps, and ending up in a fully executable functional implementation. Symmetries present in the algorithm are handled with special care.

El trabajo se presentó en el FM2012 (18th International Symposium on Formal Methods) y las transparencias de la presentación se encuentran aquí.

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