Reseña: Verifying a plaftorm for digital imaging: a multi-tool strategy

PorJosé A. Alonso

Se ha publicado un trabajo de verificación formal con Why/Krakatoa, Coq y ACL2 titulado Verifying a platform for digital imaging: a multi-tool strategy.

Sus autores son Jónathan Heras, Gadea Mata, Ana Romero, Julio Rubio y Rubén Sáenz (de la Universidad de la Rioja).

Su resumen es

Fiji is a Java platform widely used by biologists and other experimental scientists to process digital images. In particular, in our research – made together with a biologists team; we use Fiji in some pre-processing steps before undertaking a homological digital processing of images. In a previous work, we have formalised the correctness of the programs which use homological techniques to analyse digital images. However, the verification of Fiji’s pre-processing step was missed. In this paper, we present a multi-tool approach filling this gap, based on the combination of Why/Krakatoa, Coq and ACL2.

Los códigos correpondientes al trabajo se encuentran aquí.

Reseña: Formal reasoning about finite-state discrete-time Markov chains in HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre procesos de Markov titulado Formal reasoning about finite-state discrete-time Markov chains in HOL.

Sus autores son Liya Liu, Osman Hasan y Sofiène Tahar (de la Univ. de Concordia, Canadá).

Su resumen es

Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.

La revista en donde que ha publicado el artículo es el Journal of Computer Science and Technology.

Reseña: Mechanising Turing machines and computability theory in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre modelos de computación titulado Mechanising Turing machines and computability theory in Isabelle/HOL.

Sus autores son Jian Xu, Xingyuan Zhang y Christian Urban.

Su resumen es

We present a formalised theory of computability in the theorem prover Isabelle/HOL. This theorem prover is based on classical logic which precludes direct reasoning about computability: every boolean predicate is either true or false because of the law of excluded middle. The only way to reason about computability in a classical theorem prover is to formalise a concrete model of computation. We formalise Turing machines and relate them to abacus machines and recursive functions. We also formalise a universal Turing machine and Hoare-style reasoning techniques that allow us to reason about Turing machine programs. Our theory can be used to formalise other computability results.

Las teorías desarrolladas en Isabelle/HOL se encuentran en aquí.

Reseña: The Picard algorithm for ordinary differential equations in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre ecuaciones diferenciales titulado The Picard algorithm for ordinary differential equations in Coq.

Sus autores son Evgeny Makarov and Bas Spitters (de la Universidad de Nimega, Países Bajos).

Su resumen es

Ordinary Differential Equations (ODEs) are ubiquitous in physical applications of mathematics. The Picard-Lindelöf theorem is the first fundamental theorem in the theory of ODEs. It allows one to solve differential equations numerically. We provide a constructive development of the Picard-Lindelöf theorem which includes a program together with sufficient conditions for its correctness. The proof/program is written in the Coq proof assistant and uses the implementation of efficient real numbers from the CoRN library and the MathClasses library. Our proof makes heavy use of operators and functionals, functions on spaces of functions. This is faithful to the usual mathematical description, but a novel level of abstraction for certified exact real computation.

Las teorías desarrolladas se encuentran aquí.

Lecturas del Grupo de Lógica Computacional (Septiembre-Noviembre 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 septiembre de 2012. La anterior recopilación fue la de agosto 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. Operational refinement for compiler correctness. #Tesis #Coq
  2. Interactive and automated proofs for graph transformations. #Isabelle
  3. Lecturas del Grupo de Lógica Computacional (Marzo-Agosto de 2012)
  4. Piensa en Haskell (Ejercicios de programación funcional con Haskell). #Haskell
  5. ¿Computadores von Neumann, o computadores Turing? #Historia
  6. Formalizing Frankl’s conjecture: FC-families. #Isabelle
  7. Implementing an efficient theorem prover. #Tesis #Vampire
  8. System of logic based on ordinals. #Tesis #Historia
  9. Proving concurrent noninterference (código) #Isabelle
  10. Improving real analysis in Coq: a user-friendly approach to integrals and derivatives. #Coq (CPP2012)
  11. Computing persistent homology within Coq/SSReflect. #Coq
  12. Software libre para una sociedad libre. #Libro #Pensamiento
  13. A formal proof of Sasaki-Murao algorithm. #Coq (MAP2012, code, Presentación).
  14. Confluence by decreasing diagrams formalized. #Isabelle
  15. Proof Pearl – A mechanized proof of GHC’s mergesort. #Isabelle #Haskell
  16. A logic-algebraic approach to decision taking in a railway interlocking system. #BG
  17. Scheme in industrial automation. #Scheme
  18. Parallelizing an interactive theorem prover: Functional programming and proofs with ACL2. #ACL2 #Tesis
  19. A string of pearls: Proofs of Fermat’s little theorem. #HOL4
  20. A formally-verified C compiler supporting floating-point arithmetic. #Coq
  21. The Boyer-Moore waterfall model revisited. #HOL_Light
  22. A Python pattern matcher project for an introduction to Artificial Intelligence course. #IA
  23. Informatik 2: Functional Programming. #Haskell
  24. Contributions to the formal verification of arithmetic algorithms. #Tesis #Coq
  25. Why learn Haskell?. #Tutorial #Haskell
  26. A mechanical verification of the independence of Tarski’s euclidean axiom y código #Tesina #Isabelle
  27. Weak completeness theorem for propositional linear time temporal logic. #Mizar
  28. Natural language processing for the working programmer. #Haskell #IA
  29. Nexus authorization logic (NAL): Logical results. #Coq
  30. Reasons for studying Haskell in University. #Haskell
  31. Constructive completeness for modal logic with transitive closure. #Coq #Modal
  32. A functional programming approach to AI search algorithms. #IA #PF
  33. Dual multi-adjoint concept lattices. #AFC
  34. Temas de “Demostración asistida por ordenador”. #Isabelle #Tutorial
  35. Verificación de programas: Introducción. #Verificación
  36. Último dígito del producto de números de Fermat. #Haskell #IMO
  37. A formal proof of square root and division elimination in embedded programs. #PVS
  38. Coq et caractères (Preuve formelle du théorème de Feit et Thompson). #Coq #Divulgación
  39. Formalized algebraic numbers: construction and first order theory. #Tesis #Coq
  40. How enterprises use functional languages, and why they don’t. #PF
  41. Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting. #Tesis #Isabelle
  42. Constructive formalization of regular languages. #Tesina #Coq
  43. Computing with free algebras. #Haskell
  44. Ask-Elle: a Haskell Tutor. #Tesis #Haskell #TI
  45. Using Isabelle to verify special relativity, with application to hypercomputation theory. #Isabelle

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