Reseña: Fibonacci numbers and the Stern-Brocot tree in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Fibonacci numbers and the Stern-Brocot tree in Coq.

Sus autor es José Grimm (del Marelle Team en el Inria, Sophia-Antipolis Méditerranée).

Su resumen es

In this paper, we study the representation of a number by some other numbers. For instance, an integer may be represented uniquely as a sum of powers of two; if each power of two is allowed to appear at most twice, the number of representations is s(n), a sequence studied by Dijkstra, that has many nice properties proved here with the use of the proof assistant Coq. It happens that every rational number x is uniquely the quotient s(n)/s(n+1) as noticed by Stern, and that the integer n is related to the continued fraction expansion of x. It happens that by reverting the bits on n, one gets a sequence of rational numbers with increasing denominators that goes from 1 to x and becomes nearer at each iteration; this was studied by Brocot, whence the name Stern-Brocot tree. An integer can also be represented as a sum of Fibonacci numbers; we study R(n) the number of such representations; there is uniqueness for the predecessors of Fibonacci numbers; there is also uniqueness under additional constraints (for instance, no two consecutive Fibonacci numbers can be used, or no two consecutive numbers can be omitted).

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

Reseña: A framework for verified depth-first algorithms

PorJosé A. Alonso

En el CPP 2015 Peter Lammich y René Neumann presentarán el trabajo A framework for verifying depth-first search algorithms que está basado en el de René Neumann titulado A framework for verified depth-first algorithms.

El resumen de este último es

We present a framework in Isabelle/HOL for formalizing variants of depth-first search. This framework allows to easily prove non-trivial properties of these variants. Moreover, verified code in several programming languages including Haskell, Scala and Standard ML can be generated. In this paper, we present an abstract formalization of depth-first search and demonstrate how it is refined to an efficiently executable version. Further we use the emptiness-problem of Büchi-automata known from model checking as the motivation to present three Nested DFS algorithms. They are formalized, verified and transformed into executable code using our framework.

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

Reseña: Budget imbalance criteria for auctions: A formalized theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre economía titulado Budget imbalance criteria for auctions: A formalized theorem.

Sus autores son Marco B. Caminati, Manfred Kerber y Colin Rowat (de la Univ. de Birmingham).

Su resumen es

We present an original theorem in auction theory: it specifies general conditions under which the sum of the payments of all bidders is necessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theorem applies to the important case of a second-price Vickrey auction, where it reduces to a basic result of which a novel proof is given. To enhance the confidence in this new theorem, it has been formalized in Isabelle/HOL: the main results and definitions of the formal proof are re- produced here in common mathematical language, and are accompanied by an informal discussion about the underlying ideas.

El trabajo se ha presentado en la 6th Podlasie Conference on Mathematics 2014.

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

Reseña: Principles for verification tools: Separation logic

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Principles for verification tools: Separation logic

Sus autores son Brijesh Dongol, Victor B. F. Gomes y Georg Struth (de la Universidad de Sheffield).

Su resumen es

A principled approach to the design of program verification and con- struction tools is applied to separation logic. The control flow is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data flow is captured by concrete store/heap models. These are linked to the separation algebra by soundness proofs. Verification conditions and transformation laws are derived by equational reasoning within the predicate transformer quantale. This separation of concerns makes an implementation in the Isabelle/HOL proof as- sistant simple and highly automatic. The resulting tool is correct by construction; it is explained on the classical linked list reversal example.

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

Reseña: The Unified Policy Framework (UPF)

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre seguridad titulado The Unified Policy Framework (UPF)

Sus autores son

Su resumen es

We present the Unified Policy Framework (UPF), a generic framework for modelling security (access-control) policies. UPF emphasizes the view that a policy is a policy decision function that grants or denies access to resources, permissions, etc. In other words, instead of modelling the relations of permitted or prohibited requests directly, we model the concrete function that implements the policy decision point in a system. In more detail, UPF is based on the following four principles: 1) Functional representation of policies, 2) No conflicts are possible, 3) Three-valued decision type (allow, deny, undefined), 4) Output type not containing the decision only.

El marco en el que se apoya el trabajo se presenta en la tesis de Lukas Brügger A framework for modelling and testing of security policies.

El trabajo se ha publicado en The Archive of Formal Proofs.

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