BDDs verified in a proof assistant (Preliminary report)

Mathieu Giorgino and Martin Strecker


Abstract

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

PDF

Bibtex Entry

(preliminary) 

@INPROCEEDINGS{GiorginoSt2010BDDs,
  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 = {http://www.irit.fr/~Martin.Strecker/Publications/GiSt2010BDDs.html}
}