Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Gate Synthesis for C Programs with Heap

Byron Cook, Ashutosh Gupta, Satnam Singh, and Viktor Vafeiadis

Abstract

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.

Details

Publication typeProceedings
Published inDraft under submission.
PublisherIEEE Computer Society
> Publications > Gate Synthesis for C Programs with Heap