Lecturas del Grupo de Lógica Computacional (Agosto de 2011)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el mes de agosto de 2011.

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. Theorem proving for verification (the early days) #Historia
  2. Selecting attributes for sport forecasting using formal concept analysis #AFC
  3. Lecturas del Grupo de Lógica Computacional (Julio de 2011). #GLC #Vestigium
  4. Formal methods: practice and experience #Métodos_formales
  5. Automated deduction for verification #DAT
  6. Software model checking #Model_checking
  7. The verified software initiative: A Manifesto #Verificación
  8. How can i do that with ACL2 recent enhancements to ACL2 #ACL2
  9. Algebraic proofs over noncommutative formulas #Cálculo_polinomial
  10. Studies in algebraic and propositional proof complexity #Tesis #Cálculo_polinomial
  11. Formalization of an Efficient Representation of Bernstein Polynomials and Applications to Global Optimization #PVS
  12. Automating Algebraic Methods in Isabelle #Isabelle
  13. A Repository for Tarski-Kleene Algebras #Isabelle
  14. Emergence and refinement #Emergencia #Refinamentos
  15. Automated Proving in Geometry using Gröbner Bases in Isabelle/HOL #Isabelle
  16. How Efficient Can Fully Verified Functional Programs Be – A Case Study of Graph Traversal Algorithms #Isabelle
  17. Imperative functional programming with Isabelle/HOL #Isabelle
  18. A Flexible Formal Verification Framework for Industrial Scale Validation #ACL2
  19. Markets are Efficient if and Only if P = NP.
  20. Bit-Blasting ACL2 Theorems #ACL2 #GL
  21. A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. #ACL2 #GL
  22. Integrating Testing and Interactive Theorem Proving #ACL2
  23. seL4 Enforces Integrity #Isabelle
  24. Peirce’s Truth-functional Analysis and the Origin of Truth Tables. #Historia
  25. Towards Flight Control Verification Using Automated Theorem Proving #MetiTarski
  26. Ott: Effective tool support for the working semanticist. #Ott #Coq #Isabelle #HOL
  27. Lightweight Tools for Heavyweight Semantics. #Lem #Ott #Coq #Isabelle #HOL
  28. Verifying SAT and SMT in Coq for a fully automated decision procedure. #Coq #SAT #SMT
  29. Maximum Cardinality Matching. #Isabelle
  30. Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. #AA
  31. Gauss-Jordan Elimination for Matrices Represented as Functions. #Isabelle
  32. Verification of Dependable Software using Spark and Isabelle. #Isabelle
  33. Verification of Programs in Virtual Memory Using Separation Logic. #Isabelle
  34. Automated Specification Analysis Using an Interactive Theorem Prover. #ACL2
  35. Formal Analysis of Fractional Order Systems in HOL. #HOL

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

El tipo abstracto de datos de los grafos en Haskell

PorJosé A. Alonso

Continuando la serie dedicada a los tipos de datos abstractos (TAD) en Haskell, hoy le toca el turno a los grafos. En los próximos, estudiaremos algoritmos sobre grafos basados en este TAD.

Informalmente, un grafo es un conjunto de objetos llamados vértices o nodos unidos por enlaces llamados aristas o arcos.

El contenido del este artículo es el siguiente:

  • la signatura del TAD de los grafos;
  • la implementación de los grafos mediante vectores de adyacencia y
  • la implementación de los grafos mediante matrices de adyacencia.

Read More “El tipo abstracto de datos de los grafos en Haskell”

El tipo abstracto de datos de los montículos en Haskell

PorJosé A. Alonso

Continuando la serie dedicada a los tipos de datos abstractos (TAD) en Haskell, hoy le toca el turno a los montículos

Un montículo (heap en inglés) es un árbol binario en el que los valores de cada nodo es menor o igual que los valores de sus hijos. Por ejemplo,

el de la izquierda es un montículo, pero el de la derecha no lo es.

El contenido del resto del artículo es el siguiente:

  • la signatura del TAD de los montículos;
  • las propiedades del TAD de los montículos;
  • la implementación, en Haskell, de los montículos mediante tipos de datos algebraicos;
  • la comprobación con QuickCheck de sus propiedades y
  • la implementación de las colas de prioridad mediante montículos.

Read More “El tipo abstracto de datos de los montículos en Haskell”

El tipo abstracto de datos de los árboles binarios de búsqueda en Haskell

PorJosé A. Alonso

Continuando la serie dedicada a los tipos de datos abstractos (TAD) en Haskell, hoy le toca el turno a los árboles binarios de búsqueda.

Un árbol binario de búsqueda (ABB) (binary search tree en inglés) es un árbol binario tal que el valor de cada nodo es mayor que los valores de su subárbol izquierdo y es menor que los valores de su subárbol derecho y, además, ambos subárboles son árboles binarios de búsqueda. Por ejemplo, al almacenar los valores de [2,3,4,5,6,8,9] en un ABB se puede obtener los siguientes ABB:

El objetivo principal de los ABB es reducir el tiempo de acceso a los valores.

El contenido del resto del artículo es el siguiente:

  • la signatura del TAD de los árboles binarios de búsqueda;
  • las propiedades del TAD de los árboles binarios de búsqueda;
  • la implementación, en Haskell, de los árboles binarios de búsqueda mediante tipos de datos algebraicos.
  • la comprobación con QuickCheck de sus propiedades.

Read More “El tipo abstracto de datos de los árboles binarios de búsqueda en Haskell”