Gate Synthesis for C Programs with Heap

Current C to gates synthesis tools do not support programs that make non-trivial use of dynamically-allocated heap (e.g. linked-list C programs that call malloc and free). The problem is that its difficult to determine an a priori bound on the amount of heap used during the program's execution, if a bound even exists. In this paper we develop a new method of synthesizing symbolic bounds expressed over generic parameters, thus leading to a C to gates synthesis fow for programs using dynamic allocation and deallocation.

PDF file

In  Draft under submission.

Publisher  IEEE Computer Society
Copyright © 2007 IEEE. Reprinted from IEEE Computer Society. This material is posted here with permission of the IEEE. Internal or personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution must be obtained from the IEEE by writing to By choosing to view this document, you agree to all provisions of the copyright laws protecting it.


> Publications > Gate Synthesis for C Programs with Heap