Links und Funktionen

You are here: Home / Publikationen / Automatic Certification of Heap Consumption


Lennart Beringer, Martin Hofmann, Alberto Momigliano, and Olha Shkaravska (2004)

Automatic Certification of Heap Consumption

In: Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, ed. by Franz Baader and Andrei Voronkov, vol. 3452, pp. 347-362, Springer. Lecture Notes in Computer Science (ISBN: 3-540-25236-3).

We present a program logic for verifying the heap consumption of low-level programs. The proof rules employ a uniform assertion format and have been derived from a general purpose program logic$~$[1]. In a proof-carrying code scenario, the inference of invariants is delegated to the code provider, who employs a certifying compiler that generates a certificate from program annotations and analysis. The granularity of the proof rules matches that of the linear type system presented in$~$[6], which enables us to perform verification by replaying typing derivations in a theorem prover, given the specifications of individual methods. The resulting verification conditions are of limited complexity, and are automatically discharged. We also outline a proof system that relaxes the linearity restrictions and relates to the type system of usage aspects presented in$~$[2].

Document Actions