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 . 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 , 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 .
|Titolo:||Automatic Certification of Heap Consumption|
MOMIGLIANO, ALBERTO (Penultimo)
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
|Data di pubblicazione:||2005|
|Digital Object Identifier (DOI):||10.1007/978-3-540-32275-7_23|
|Tipologia:||Book Part (author)|
|Appare nelle tipologie:||03 - Contributo in volume|