Reseña: “Computational verification of network programs in Coq”

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en Coq titulado Computational verification of network programs in Coq.

Su autor es Gordon Stewart (miembro del proyecto Verified Software Toolchain la Universidad de Princeton).

Su resumen es

We report on the design of the first fully automatic, machine-checked tool suite for verification of high-level network programs. The tool suite targets programs written in NetCore, a new declarative network programming language. Our work builds on a recent effort by Guha, Reitblatt, and Foster to build a machine-verified compiler from NetCore to OpenFlow, a new protocol for software-defined networking. The result is an end-to-end system that provides strong guarantees on the compiled OpenFlow flow tables that are installed on actual network switches.

El correspondiente código en Coq se encuentra aquí.

Lecturas del Grupo de Lógica Computacional (Junio de 2013)

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 enero de 2013. La anterior recopilación fue la de diciembre 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. Problemas sobre el 2013 en Haskell. #Haskell
  2. La sucesión de Perrin en Haskell. #Haskell
  3. Representación de 2ⁿ como 7x²+y² (con x e y impares) en Haskell #Haskell
  4. Computing square roots using the babylonian method. #Isabelle
  5. Formal verification of nonlinear inequalities with Taylor interval approximations. #HOL_Light
  6. Characteristic formulae for mechanized program verification. #Tesis #Coq
  7. Construction and stochastic applications of measure spaces in Higher-Order Logic. #Tesis #Isabelle
  8. A proof of Bertrand’s postulate. #Matita
  9. Trusting computations: a mechanized proof from partial differential equations to actual program. #Coq
  10. Formal construction of a set theory in Coq. #Tesis #Coq
  11. Rank-nullity theorem in linear algebra. #Isabelle #AFP
  12. GDT4MAS: a formal model and language to specify and verify agent-based complex systems. #PVS
  13. Kleene algebra. #AFP #Isabelle
  14. Information-theoretic analysis using theorem proving. #Tesis #HOL4
  15. Applying formal methods in software development. #Tesis #PVS
  16. Formalization and concretization of ordered networks. #Coq
  17. The design of a practical proof checker for a lazy functional language. #MProver #Haskell
  18. The formalization of syntax-based mathematical algorithms using quotation and evaluation
  19. A verified decision procedure for MSO on words based on derivatives of regular expressions. #Isabelle
  20. Statistical proof-patterns in Coq/SSReflect. #Coq
  21. Towards a logic-based unifying framework for computing.
  22. Termination tools in automated reasoning. #Tesis
  23. Matrices à blocs et en forme canonique. #Coq
  24. Automated verification of termination certificates. #Coq
  25. Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
  26. Towards self-verification of Isabelle’s Sledgehammer. #Isabelle
  27. A framework for the verification of certifying computations. #Isabelle
  28. A preliminary univalent formalization of the p-adic numbers. #Coq
  29. Algunos vínculos entre los teoremas de Gödel y Turing
  30. Formal computations and methods. #Tesis #HOL_Light
  31. Complex concept lattices for simulating human prediction in sport.
  32. MaSh: Machine learning for Sledgehammer. #Isabelle #ITP2013
  33. Une étude formelle de la théorie des calculs locaux à l’aide de l’assistant de preuve Coq. #Tesis #Coq
  34. Temas de programación lógica e inteligencia artificial. #Prolog
  35. Una curiosa propiedad del 123 en Haskell. #Haskell
  36. A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2. #Isabelle #ACL2
  37. Otra curiosa propiedad del 123 en Haskell. #Haskell
  38. Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos. #PVS
  39. Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle
  40. ML4PG: proof-mining in Coq. #Coq
  41. Concept-forming operators on multilattices. #AFC
  42. The gauge integral theory in HOL4. #HOL4
  43. The Picard algorithm for ordinary differential equations in Coq. #Coq
  44. Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle #ITP2013
  45. Formal reasoning about finite-state discrete-time Markov chains in HOL. #HOL
  46. Verifying a plaftorm for digital imaging: a multi-tool strategy. #Coq #ACL2
  47. Deducción natural en lógica proposicional con Isabelle/HOL. #Isabelle
  48. Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
  49. Knowledge representation, reasoning, and the design of intelligent agents. #Libro #ASP
  50. A hierarchy of mathematical structures in ACL2. #ACL2
  51. Programming and reasonning with powerlists in Coq. #Coq
  52. Formalization of the complex number theory in HOL4. #HOL4
  53. Formalizing the confluence of orthogonal rewriting systems. #PVS
  54. Homotopy limits in Coq. #Coq
  55. Data refinement in Isabelle/HOL. #Isabelle_HOL
  56. Formalization of real analysis: A survey of proof assistants and libraries. #ITP
  57. AI over large formal knowledge bases: The first decade. #Mizar
  58. ForMaRE-formal mathematical reasoning in economics.
  59. A fully verified executable LTL model checker. #Isabelle
  60. Automating inductive proofs using theory exploration. #Haskell #HipSpec
  61. One logic to use them all. #CADE24 #Why3
  62. Square root and division elimination in PVS. #PVS #ITP2013
  63. Experience report: Teaching Haskell to the masses. #Haskell
  64. Coinductive pearl: Modular first-order logic completeness. #Isabelle
  65. Formalization of incremental simplex algorithm by stepwise refinement. #Isabelle
  66. Les assistants de preuve, ou comment avoir confiance en ses démonstrations. #DAO
  67. Developing an auction theory toolbox. #Isabelle
  68. Formalizing Knuth-Bendix orders and Knuth-Bendix completion. #Isabelle
  69. A formal proof of Kruskal’s tree theorem in Isabelle/HOL. #Isabelle
  70. A constructive theory of regular languages in Coq. #Coq
  71. A machine-checked proof of the odd order theorem. #Coq
  72. Graph theory. #Isabelle #AFP
  73. A macro for reusing abstract functions and theorems. #ACL2
  74. Light-weight containers for Isabelle: efficient, extensible, nestable. #Isabelle
  75. Formalizing Turing machines. #Matita
  76. A certified reduction strategy for homological image processing. #Coq
  77. On the formalization of continuous-time Markov chains in HOL. #HOL
  78. A Web interface for Isabelle: The next generation. #Isabelle #CICM2013
  79. Verifying refutations with extended resolution. #ACL2
  80. Type classes and filters for mathematical analysis in Isabelle/HOL. #Isabelle
  81. Mechanical verification of SAT refutations with extended resolution. #ACL2 #ITP2013
  82. The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups). #Coq
  83. Automatic data refinement. #Isabelle #ITP2013
  84. Certified HLints with Isabelle/HOLCF-Prelude. #Isabelle
  85. Theorem of three circles in Coq. #Coq
  86. A Haskell library for term rewriting. #Haskell
  87. Formal mathematics on display: A wiki for Flyspeck. #HOL_Light
  88. Solveurs CP(FD) vérifiés formellement. #Coq
  89. Formalizing bounded increase. #Isabelle
  90. Certified symbolic manipulation: Bivariate simplicial polynomials. #ACL2
  91. The formalization of syntax-based mathematical algorithms using quotation and evaluation.
  92. Homotopy type theory: Univalent foundations of mathematics. #Libro
  93. Mathematicians think like machines for perfect proofs.
  94. Certifying homological algorithms to study biomedical images. #Tesis #Coq #Haskell
  95. Formalizing cut elimination of coalgebraic logics in Coq. #Coq

La recopilación de las lecturas anteriores se encuentra aquí.

Reseña: “Formalizing cut elimination of coalgebraic logics in Coq”

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre metalógica titulado Formalizing cut elimination of coalgebraic logics in Coq.

Su autor es Hendrik Tews (de la Dresden University of Technology) y se presentará en el Tableaux 2013 (Automated Reasoning with Analytic Tableaux and Related Methods).

Su resumen es

In their work on coalgebraic logics, Pattinson and Schröder prove soundness, completeness and cut elimination in a generic sequent calculus for propositional multi-modal logics. The present paper reports on a formalization of Pattinson’s and Schröder’s work in the proof assistant Coq that provides machine-checked proofs for soundness, completeness and cut elimination of their calculus. The formalization exploits dependent types to obtain a very concise deep embedding for formulas and proofs. The work presented here can be used to verify cut elimination theorems for different modal logics with considerably less effort in the future.

El código de las correspondientes teorías en Coq se encuentra aquí.

Coq gana el “2013 ACM SIGPLAN Software System Award”

PorJosé A. Alonso

El sistema de demostración asistida Coq ha recibido este año el premio Programming Languages Software Award del grupo SIGPLAN (Special Interest Group in Programing Languages) de la ACM (Association for Computing Machinery).

La justificación del premio a Coq es la siguiente:

The Coq proof assistant provides a rich environment for interactive development of machine-checked formal reasoning. Coq is having a profound impact on research on programming languages and systems, making it possible to extend foundational approaches to unprecedented levels of scale and confidence, and transfer them to realistic programming languages and tools. It has been widely adopted as a research tool by the programming language research community, as evidenced by the many papers at SIGPLAN conferences whose results have been developed and/or verified in Coq. It has also rapidly become one of the leading tools of choice for teaching the foundations of programming languages, with courses offered by many leading universities and a growing number of books emerging to support them. Last but not least, these successes have helped to spark a wave of widespread interest in dependent type theory, the richly expressive core logic on which Coq is based.

As a software system, Coq has been in continuous development for over 20 years, a truly impressive feat of sustained, research-driven engineering. The Coq team continues to develop the system, bringing significant improvements in expressiveness and usability with each new release.

In short, Coq is playing an essential role in our transition to a new era of formal assurance in mathematics, semantics, and program verification.