up: Publications

Correctness of pointer manipulating algorithms illustrated by a verified BDD construction

Mathieu Giorgino, Martin Strecker

FM 2012


This paper is an extended case study using a high-level approach to the verification of graph transformation algorithms: To represent sharing, graphs are considered as trees with additional pointers, and algorithms manipulating them are essentially primitive recursive traversals written in a monadic style. With this, we achieve almost trivial termination arguments and can use inductive reasoning principles for showing the correctness of the algorithms. We illustrate the approach with the verification of a BDD package which is modular in that it can be instantiated with different implementations of association tables for node lookup. We have also implemented a garbage collector for freeing association tables from unused entries. Even without low-level optimizations, the resulting implementation is reasonably efficient.
 Online Copy

Conference version: PDF

BibTeX Entry

   author = {Giorgino, Mathieu and Strecker, Martin},
   affiliation = {IRIT, Université de Toulouse, France},
   title = {Correctness of Pointer Manipulating Algorithms Illustrated by a Verified {BDD} Construction},
   booktitle = {FM 2012: Formal Methods},
   series = {Lecture Notes in Computer Science},
   editor = {Giannakopoulou, Dimitra and Méry, Dominique},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-642-32758-2},
   keyword = {Computer Science},
   pages = {202-216},
   volume = {7436},
   doi = {http://dx.doi.org/10.1007/978-3-642-32759-9_18},
   url = {http://www.irit.fr/~Martin.Strecker/Publications/fm2012.html},
   year = {2012}

Last modified: Wed Aug 8 15:36:28 CEST 2012