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].
Automatic Certification of Heap Consumption / L. Beringer, M. Hofmann, A. Momigliano, O. Shkaravska (LECTURE NOTES IN COMPUTER SCIENCE). - In: Logic for Programming, Artificial Intelligence, and Reasoning / [a cura di] F. Baader, A. Voronkov. - Berlin : Springer, 2005. - ISBN 9783540252368. - pp. 347-362 (( Intervento presentato al 11. convegno International Conference on Logic for Programming, Artificial Intelligence, and Reasoning tenutosi a Montevideo nel 2005 [10.1007/978-3-540-32275-7_23].
Automatic Certification of Heap Consumption
A. MomiglianoPenultimo
;
2005
Abstract
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].File | Dimensione | Formato | |
---|---|---|---|
heap.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
197.96 kB
Formato
Adobe PDF
|
197.96 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.