Refinements for free!

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre refinamientos de datos titulado Refinements for free!.

Sus autores son

Su resumen es

Formal verification of algorithms often requires a choice between definitions that are easy to reason about and definitions that are computationally efficient. One way to reconcile both consists in adopting a high-level view when proving correctness and then refining stepwise down to an efficient low-level implementation. Some refinement steps are interesting, in the sense that they improve the algorithms involved, while others only express a switch from data representations geared towards proofs to more efficient ones geared towards computations. We relieve the user of these tedious refinements by introducing a framework where correctness is established in a proof-oriented context and automatically transported to computation-oriented data structures. Our design is general enough to encompass a variety of mathematical objects, such as rational numbers, polynomials and matrices over refinable structures. Moreover, the rich formalism of the Coq proof assistant enables us to develop this within Coq, without having to maintain an external tool.

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

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.