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. © 2012 Springer-Verlag.
CITATION STYLE
Giorgino, M., & Strecker, M. (2012). Correctness of pointer manipulating algorithms illustrated by a verified BDD construction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7436 LNCS, pp. 202–216). https://doi.org/10.1007/978-3-642-32759-9_18
Mendeley helps you to discover research relevant for your work.