Reseña: Proving concurrent noninterference

PorJosé A. Alonso

En la CPP 2012 (The Second International Conference on Certified Programs and Proofs), que comenzará el 13 de diciembre, se presentará un trabajo de verificación formal en Isabelle/HOL titulado Proving concurrent noninterference.

Sus autores son Andrei Popescu, Johannes Hölzl y Tobias Nipkow (del grupo de demostración automática (Theorem Proving Group) de la Universidad de Munich).

Su resumen es

We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of noninterference variants from the literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL.

Este trabajo forma parte del proyecto Security Type Systems and Deduction

El código con las teorías correspondiente se encuentra aquí.

Reseña: Formalizing Frankl’s conjecture: FC-families

PorJosé A. Alonso

En las CICM 2012 (Conferences on Intelligent Computer Mathematics) se ha presentado un trabajo de razonamiento formalizado en Isabelle/HOL titulado Formalizing Frankl’s conjecture: FC-families.

Sus autores son Filip Marić, Miodrag Živković y Bojan Vučković (del grupo ARGO (Automated Reasoning GrOup) de la Universidad de Belgrado).

Su resumen es

The Frankl’s conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. FC-families are families for which it is proved that every union-closed family containing them satisfies the Frankl’s condition (e.g., in every union-closed family that contains a one- element set a, the element a is contained in at least half of the sets, so families of the form a are the simplest FC-families). FC-families play an important role in attacking the Frankl’s conjecture, since they enable significant search space pruning. We present a formalization of the computer assisted approach for proving that a family is an FC-family. Proof-by-computation paradigm is used and the proof assistant Isabelle/HOL is used both to check mathematical content, and to perform (verified) combinatorial searches on which the proofs rely. FC-families known in the literature are confirmed, and a new FC-family is discovered.

El código con la formalización en Isabelle/HOL se encuentra aquí.

PeH: Piensa en Haskell (Ejercicios de programación funcional con Haskell)

PorJosé A. Alonso

He publicado la primera versión de libro Piensa en Haskell (Ejercicios de programación funcional con Haskell).

Este libros es una introducción a la programación funcional con Haskell a través de una colección de ejercicios resueltos de los cursos de Informática (del
Grado en Matemáticas) y Programación declarativa (de la Ingeniería en Informática).

Los temas correspondientes a los ejercicios del libro se encuentra en Temas de programación funcional.

El libro consta de tres partes. En la primera parte se presentan los elementos básicos de la programación funcional. En la segunda, se estudian la implementación en Haskell de tipos abstractos de datos y sus aplicaciones así como cuestiones algorítmicas. En la tercera, se presentan casos de estudios. También se han incluido dos apéndices: uno con un resumen de las funciones de Haskell utilizadas y otro con el método de Pólya para la resolución de problemas.
Read More “PeH: Piensa en Haskell (Ejercicios de programación funcional con Haskell)”

Lecturas del Grupo de Lógica Computacional (Marzo-Agosto de 2012)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el mes de marzo de 2012. La anterior recopilación fue la de febrero de 2012.

La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

  1. Automatic proofs and refutations for higher-order logic. #Tesis #Isabelle
  2. On theorem prover-based testing. #Isabelle
  3. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. #Coq
  4. Tips on Haskell. #Tutorial #Haskell
  5. Enfragmo: A system for modelling and solving search problems with logic. #SAT
  6. Logic & reasoning: from Aristotle to Intel. #Panorama #Lógica
  7. Deciding Kleene Algebras in Coq. #Coq
  8. Vérification semi-automatique de primitives cryptographiques. #Tesis #Coq
  9. Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model. #PVS
  10. Formal error analysis and verification of the frequency domain equalizer. #HOL
  11. Introduction to the Coq proof-assistant for practical software verification. #Tutorial #Coq
  12. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination #Coq
  13. Mathematics for Computer Science. #Libro
  14. Proving possibilistic, probabilistic noninterference. #Isabelle
  15. Decision procedures in Algebra and Logic (Reading material). #Libro #Lógica
  16. A formalization of the theorem of existence of first-order most general unifiers. #PVS
  17. The worldʼs shortest correct exact real arithmetic program?. #PVS #Haskell
  18. Kleene algebra, rewriting modulo AC and circuits in Coq. #Tesis #Coq
  19. Deriving a fast inverse of the generalized Cantor n-tupling bijection. #Prolog
  20. PVS linear algebra libraries for verification of control software algorithms in C/ACSL. #PVS
  21. Generating verifiable Java code from verified PVS specifications. #PVS
  22. Haskell gets argumentative. #Haskell #Lógica @IA
  23. Induction and recursion. #Fundamentos
  24. A formal proof of Sasaki-Murao algorithm. #Coq
  25. Essential incompleteness of arithmetic verified by Coq. #Coq
  26. Incompleteness & completeness: Formalizing logic and analysis in type theory. #Tesis #Coq
  27. Well-quasi-orders. #Isabelle
  28. Analyse et Conception Formelles (Software formal analysis and design). #Curso #Isabelle
  29. Programming and proving in Isabelle/HOL. #Isabelle
  30. Numerical analysis of ordinary differential equations. #Isabelle
  31. Inductive study of confidentiality. #AFP #Isabelle
  32. Formal correctness of security protocols. #Libro #Isabelle
  33. Stuttering equivalence. #AFP
  34. HaskHOL: A Haskell hosted domain specific language for Higher-Order Logic theorem proving. #Tesis #Haskell
  35. A string of pearls: proofs of Fermat’s little theorem. #HOL4
  36. Separation logic: A logic for shared mutable data structures.
  37. Local action and abstract separation logic.
  38. Separation algebra. #Isabelle
  39. Using PVS to support the analysis of distributed cognition systems. #PVS
  40. Formal verification of the heavy hitter problem. #HOL
  41. Formal probabilistic analysis using theorem proving. #Tesis #HOL
  42. Proving equational Haskell properties using automated theorem provers. #Haskell #Thesis
  43. Accessible integrated formal reasoning environments in classroom instruction of mathematics.
  44. Designing accessible lightweight formal verification systems.
  45. Artificial intelligence: from fantasy to reality. #IA
  46. HipSpec: Automating inductive proofs of program properties. #Haskell
  47. Supplementary material for “Thinking as computation”. #IA #Prolog
  48. Verifying an algorithm computing discrete vector fields for digital imaging. #Coq
  49. Bridging the gap: Automatic verified abstraction of C
  50. Computing in Cantor’s paradise with λZFC.
  51. Thoughts on gamifying textbooks.
  52. Isabelle/Circus: A process specification and verification environment. #Isabelle
  53. Isabelle/Circus. #Isabelle
  54. Wave equation numerical resolution: a comprehensive mechanized proof of a C program #Coq
  55. Large-scale formal verification in practice: A process perspective. #Isabelle
  56. A framework for formally verifying software transactional memory algorithms. #PVS
  57. Rigorous polynomial approximation using Taylor models in Coq. #Coq
  58. Rigorous polynomial approximations and applications. #Tesis #Coq
  59. Seventy four minutes of mathematics: An analysis of the third Mini-Polymath project. #MKM
  60. Formalizing Kruskal’s tree theorem in Isabelle/HOL. #Isabelle
  61. Verifying an algorithm computing discrete vector fields for digital imaging. #Coq
  62. Formal verification of monad transformers. #Isabelle
  63. HALO: Haskell to logic through denotational semantics. #Haskell
  64. Interactive proof: Introduction to Isabelle/HOL. #Tutorial #Isabelle
  65. Formalization of an efficient representation of Bernstein polynomials and applications to global optimization #PVS
  66. Lifting and transfer: A modular design for quotients in Isabelle/HOL. #Isabelle
  67. Meta-theory à la carte. #Coq
  68. Mechanization of an algorithm for deciding KAT terms equivalence. #Coq
  69. ¿Es posible construir software que no falle?. #Verificación
  70. Proving the impossibility of trisecting an angle and doubling the cube. #Isabelle
  71. Formal specification and verification of well-formedness in business process product lines. #PVS
  72. Compiling concurrency correctly (Verifying software transactional memory). #Tesis #Agda #Haskell
  73. Représentation coinductive des graphes. #Tesis #Coq
  74. Formalizing adequacy: A case study for higher-order abstract syntax. #Isabelle
  75. Algorithms in games evolving in time: Winning strategies based on testing. #Isabelle
  76. A certified JavaScript interpreter. #Coq
  77. Formalization of Shannon’s theorems in SSReflect-Coq. #Coq
  78. Abstract interpretation of annotated commands. #Isabelle
  79. Construction of real algebraic numbers in Coq. #Coq
  80. Correctness of pointer manipulating algorithms illustrated by a verified BDD construction. #Isabelle
  81. Towards provably robust watermarking. #Coq
  82. Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL. #Isabelle
  83. Formalizing an abstract algebra textbook in Isabelle/HOL. #Isabelle
  84. Numerical analysis of ordinary differential equations in Isabelle/HOL. #Isabelle
  85. A refinement-based approach to computational algebra in Coq. #Coq
  86. Coherent and strongly discrete rings in type theory. #Coq
  87. Logic + control: An example of program construction. #Prolog
  88. Deriving a fast inverse of the generalized Cantor N-tupling bijection. #Prolog
  89. Formalization and verification of number theoretic algorithms using the Mizar proof checker. #Mizar

En Mendeley también se encuentran las lecturas del Grupo de Lógica Computacional.