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]. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Beringer, L., Hofmann, M., Momigliano, A., & Shkaravska, O. (2005). Automatic certification of heap consumption. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3452 LNAI, pp. 347–362). Springer Verlag. https://doi.org/10.1007/978-3-540-32275-7_23
Mendeley helps you to discover research relevant for your work.