up: Publications

BDDs verified in a proof assistant (Preliminary report)

Mathieu Giorgino, Martin Strecker


This paper is a case study in mechanical verification of graph manipulating algorithms: We prove the correctness of a family of algorithms constructing Binary Decision Diagrams in a monadic style. It distinguishes itself from previous verification efforts in two respects: Firstly, building the BDD structure is guided by a primitive recursive descent which makes the proof of termination trivial. Secondly, the development is modular: it is parametrized by primitives manipulating high-level hash tables that can be realized by several implementations.
Online Copy


BibTeX Entry

  author =       {Giorgino, Mathieu and Strecker, Martin},
  title =        {{BDDs} verified in a proof assistant (Preliminary report)},
  booktitle = {Proc. TAAPSD},
  year =      2010,
  editor =    {A.V. Anisimov and M.S. Nikitchenko},
  address =   {Univ. Taras Shevchenko, Kiev},
  url = {https://www.irit.fr/~Martin.Strecker/Publications/taapsd10.html}

Last modified: Thu Sep 2 14:42:56 CEST 2010