Verifying linearizability with Hindsight
Peter W. O'Hearn, Noam Rinetzky, et al.
PODC 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.
Peter W. O'Hearn, Noam Rinetzky, et al.
PODC 2010
Olga Brukman, Shlomi Dolev, et al.
Journal of Systems and Software
David F. Bacon, Perry Cheng, et al.
EMSOFT 2005
Hana Chockler, Karine Even, et al.
ISSTA 2013