En la segunda parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los primeros 9 ejercicios 2ª relación sobre definiciones por composición de funciones sobre listas.
Los ejercicios y su solución se muestran a continuación
Read More “I1M2013: Ejercicios de definiciones por composición de funciones sobre listas”
En la primera parte de la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se estudiado cómo definir funciones eh Haskell usando los formas básicas: composición, condicionales, guardas y patrones.
Las transparencias usadas en la clase son las páginas 1-14 del tema 4:
Read More “I1M2013: Definición de funciones elementales en Haskell”
Se ha publicado un artículo de razonamiento formalizado en PVS titulado The ontological argument in PVS.
Su autor es John Rushby (del SRI International).
Su resumen es
The Ontological Argument, an 11th Century proof of the existence of God, is a good candidate for Fun With Formal Methods as nearly everyone finds the topic interesting. We formalize the Argument in PVS and verify its correctness. The formalization raises delicate questions in formal logic and provides an opportunity to show how these are handled, soundly and efficiently, by the predicatively-subtyped higher-order logic of PVS and its mechanized support. The simplicity of the Argument, coupled to its bold conclusion, raise interesting issues on the interpretation and application of formal methods in the real world.
Se ha publicado un artículo de razonamiento formalizado en Nuplr titulado Formalizing Moessner’s theorem and generalizations in Nuprl.
Sus autores son
Su resumen es
Moessner’s theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers
. Several generalizations of Moessner’s theorem exist. Recently, Kozen and Silva gave an algebraic proof of a general theorem that subsumes Moessner’s original theorem and its known generalizations. In this note, we describe the formalization of this theorem that the first author did in Nuprl. To the best of our knowledge, this is the first existing machine formalization. On the one hand, the formalization remains remarkably close to the original proof. On the other hand, it leads to new insights in the proof, pointing to small gaps and ambiguities that would never raise any objections in pen and pencil proofs, but which must be resolved in machine formalization.
Se ha publicado en el JFR un artículo de razonamiento formalizado en PVS titulado Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model.
Sus autores son Mauricio Ayala Rincón y Yuri Santos Rêgo (de la Univ. de Brasilia).
Su resumen es
In this work, we present an algebraic approach for modeling the two-party cascade protocol of Dolev-Yao and for fully formalizing its security in the specification language of the Prototype Verification System PVS. Although cascade protocols could be argued to be a very limited model, it should be stressed here that they are the basis of more sophisticated protocols of great applicability, such as those which allow treatment of multiparty, tuples, nonces, name-stamps, signatures, etc. In the current algebraic approach, steps of the protocol are modeled in a monoid freely generated by the cryptographic operators. Words in this monoid are specified as finite sequences and the whole protocol as a finite sequence of protocol steps, that are functions from pairs of users to sequences of cryptographic operators. In a previous work, assuming that for balanced protocols admissible words produced by a potential intruder should be balanced, a formalization of the characterization of security of this kind of protocols was given in PVS. In this work, the previously assumed property is also formalized, obtaining in this way a complete formalization which mathematically guarantees the security of these protocols. Despite such property being relatively easy to specify, obtaining a complete formalization requires a great amount of effort, because several algebraic properties, that are related to the preservation of the balancing property of the admissible language of the intruder, should be formalized in the granularity of the underlying data structure (of finite sequences used in the specification). Among these properties, the most complex are related to the notion of linkage property, which allows for a systematic analysis of words of the admissible language of a potential saboteur, showing how he/she is unable to isolate private keys of other users under the assumption of balanced protocols. The difficulties that can arise in conducting this formalization are also presented in this work.
La teorías PVS correspondientes se encuentran en aquí.