Abstraction-guided synthesis of synchronization
Martin Vechev, Eran Yahav, et al.
POPL 2010
We present a framework for statically reasoning about temporal heap safety properties. We focus on local temporal heap safety properties, in which the verification process may be performed for a program object independently of other program objects. We apply our framework to produce new conservative static algorithms for compile-time memory management, which prove for certain program points that a memory object or a heap reference will not be needed further. These algorithms can be used for reducing space consumption of Java programs. We have implemented a prototype of our framework, and used it to verify compile-time memory management properties for several small, but interesting example programs, including JavaCard programs. © 2005 Elsevier B.V. All rights reserved.
Martin Vechev, Eran Yahav, et al.
POPL 2010
Michael Factor, David Hadas, et al.
MSST 2013
Harel Paz, Erez Petrank, et al.
CC - ETAPS 2005
Marco Pistoia, Stephen J. Fink, et al.
ICSE 2007