up: Publications |
Abstract |
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 |
@incollection{giorgino12:_correc_bdd, 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 = {https://www.irit.fr/~Martin.Strecker/Publications/fm2012.html}, year = {2012} }
Last modified: Wed Aug 8 15:36:28 CEST 2012 |