Aliasing restrictions of C11 formalized in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre la semántica del lenguaje C titulado Aliasing restrictions of C11 formalized in Coq.

Su autor es Robbert Krebbers (de la Radboud University Nijmegen, Holanda).

Su resumen es

The C11 standard of the C programming language describes dynamic typing restrictions on memory operations to make more effective optimizations based on alias analysis possible. These restrictions are subtle due to the low-level nature of C, and have not been treated in a formal semantics before. We present an executable formal memory model for C that incorporates these restrictions, and at the same time describes required low-level operations.

Our memory model and essential properties of it have been fully formalized using the Coq proof assistant.

Este trabajo forma parte del proyecto CH₂O cuyo objetivo es la formalización del estándard C11 del lenguaje de programación C.

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 Coq se encuentra aquí.

RA2013: Razonamiento por casos y por inducción (1)

PorJosé A. Alonso

La clase de hoy del curso de Razonamiento automático ha tenido dos partes: comentar las soluciones de los ejercicios de la relación 4 y empezar el estudio del tema 4.

En la relación 4 se define la función cons que añade un elemento al final de la lista y se demuestra algunas de sus propiedades. Lo interesante es el uso de algunas propiedades en la demostración de otras (como en el ejercicio 5). Las ejercicios y sus soluciones son
Read More “RA2013: Razonamiento por casos y por inducción (1)”

Formalizing probabilistic noninterference

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Formalizing probabilistic noninterference

Sus autores son Andrei Popescu, Johannes Hölzl y Tobias Nipkow (de la Universidad Técnica de Munich, Alemania).

Su resumen es

We present an Isabelle formalization of probabilistic noninterference for a multi-threaded language with uniform scheduling. Unlike in previous settings from the literature, here probabilistic behavior comes from both the scheduler and the individual threads, making the language more realistic and the mathematics more challenging. We study resumption-based and trace-based notions of probabilistic noninterference and their relationship, and also discuss compositionality w.r.t. the language constructs and type-system-like syntactic criteria. The formalization uses recent development in the Isabelle probability theory library.

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 se encuentra aquí.

LI2013: Tableros semánticos de primer orden y equivalencias lógicas

PorJosé A. Alonso

En la primera parte de la clase de hoy del curso Lógica Informática se ha presentado un nuevo sistema deductivo: los tableros semánticos de primer orden como ampliación del presentado en el tema 3 para la lógica proposicional.

En la segunda parte, se ha demostrado por deducción natural las principales equivalencias en lógica de primer orden. Además, se ha mostrado cómo hacer las demostraciones en Pandora como se muestra en este vídeo.

Las transparencias de esta clase son las finales del tema 8 y las del tema 9 que se muestran a continuación
Read More “LI2013: Tableros semánticos de primer orden y equivalencias lógicas”

I1M2013: Ejercicios de definiciones por recursión y comprensión (2)

PorJosé A. Alonso

En la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se han comentado las soluciones de los ejercicios 6 a 17 de la 10ª relación y los de la 11ª. En ambas relaciones se proponen ejercicios con dos definiciones (una por recursión y otra por comprensión) y la comprobación de la equivalencia de las dos definiciones con QuickCheck.

Los ejercicios 6 a 17 de la relación 10 y soluciones se muestran a continuación
Read More “I1M2013: Ejercicios de definiciones por recursión y comprensión (2)”