Certified Kruskal’s tree theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre órdenes titulado Certified Kruskal’s tree theorem.

Su autor es Christian Sternagel (del Japan Advanced Institute of Science and Technology).

Su resumen es

This paper gives the first formalization of Kruskal’s tree theorem in a proof assistant. More concretely, an Isabelle/HOL development of Nash-Williams’ minimal bad sequence argument for proving the tree theorem is presented. Along the way, the proofs of Dickson’s lemma and Higman’s lemma are discussed.

El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).

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

Formal modeling and verification (in PVS) of multi-agent system architecture

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en PVS sobre multi agentes titulado Formal modeling and verification of multi-agent system architecture.

Sus autores son

  • Ling Yuan (de la Huazhong University of Science and Technology, Wuhan, China) y
  • Ping Fan (de la Hubei University of Science and Technology, Hubei, China).

Su resumen es

In a multi-agent system, the multiple distributed intelligent agents interact with each other to solve problems. To guide the development of multi-agent system, the multi-agent system architecture would provide a framework. The specific multi- agent system can be customized from the multi-agent system architecture, which does not need to rewrite the construction. In order to satisfy the failure recovery property of multi-agent system, we propose dependable multi-agent system architecture with fault tolerant mechanisms. The PVS formal language is used to build a system architecture, which can provide common patterns and idioms to the system developers. In order to satisfy the reliability requirements, the powerful PVS theorem prover can be used to analyze the high reliability property of the proposed architecture.

El trabajo se ha presentado en la 2013 AASRI Conference on Parallel and Distributed Computing and Systems.

Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre
teoría de grafos titulado Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem.

Su autor es Lars Noschinski (de la Universidad Técnica de Munich, Alemania).

Su resumen es

The Girth-Chromatic number theorem is a theorem from graph theory, stating that graphs with arbitrarily large girth and chro- matic number exist. We formalize a probabilistic proof of this theorem in the Isabelle/HOL theorem prover, closely following a standard textbook proof and use this to explore the use of the probabilistic method in a theorem prover.

El trabajo se presentó en el ITP 2012 (Interactive Theorem Proving).

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

Reseña: A graph library for Isabelle

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle titulado A graph library for Isabelle.

Su autor es Lars Noschinski (de la Universidad Técnica de Munich, Alemania).

Su resumen es

In contrast to other areas of such as analysis, number theory or probability theory, no standard library for graph theory has yet evolved for the Isabelle/HOL proof assistant. We present a formalization of directed graphs and essential related concepts. The library supports general infinite directed graphs (digraphs) with labeled and parallel arcs, but care has been taken not to complicate reasoning on more restricted classes of digraphs.

We use this library to formalize a characterization of Euler Digraphs and a to verify a method of checking Kuratowski subgraphs used in the LEDA library.

El código de la teoría en Isabelle se encuentra aquí.

Applications of real number theorem proving in PVS

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con PVS titulado Applications of real number theorem proving in PVS.

Sus autores son

Su resumen es

Real number theorem proving has many uses, particularly for verification of safety critical systems and systems for which design errors may be costly. We discuss a chain of developments building on real number theorem proving in PVS. This leads from the verification of aspects of an air traffic control system, through work on the integration of computer algebra and automated theorem proving to a new tool, NRV, first presented here that builds on the capabilities of Maple and PVS to provide a verified and automatic analysis of Nichols plots. This automates a standard technique used by control engineers and greatly improves assurance compared with the traditional method of visual inspection of the Nichols plots.