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. Momigliano
Penultimo
;
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].
Proving pointer programs; in-place update; logic; verification
Settore INF/01 - Informatica
Book Part (author)
File in questo prodotto:
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

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/212770
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 32
  • ???jsp.display-item.citation.isi??? 30
social impact