up: Publications |
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 |
BibTeX Entry |
@InProceedings{giorgino10:_bdds_taapsd, 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/taapsd10.html} }
Last modified: Thu Sep 2 14:42:56 CEST 2010 |