id: 02227666
dt: a
an: 02227666
au: Beringer, Lennart; Hofmann, Martin; Momigliano, Alberto; Shkaravska, Olha
ti: Automatic certification of heap consumption.
so: Baader, Franz (ed.) et al., Logic for programming, artificial intelligence,
    and reasoning. 11th international conference, LPAR 2004, Montevideo,
    Uruguay, March 14‒18, 2005. Proceedings. Berlin: Springer (ISBN
    3-540-25236-3/pbk). Lecture Notes in Computer Science 3452. Lecture
    Notes in Artificial Intelligence, 347-362 (2005).
py: 2005
pu: Berlin: Springer
la: EN
cc: 
ut: 
ci: Zbl 1077.68565
li: doi:10.1007/b106931
ab: Summary: 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
    [{\it M. Hofmann} and {\it S. Jost}, “Static prediction of heap space
    usage for first-order functional programms", Proc. of POPL’03,
    185‒197 (2003)], 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 [{\it D.
    Aspinall} and {\it M. Hofmann}, “Another type system for in-place
    update", Lect. Notes Comput. Sci. 2305, 36‒52 (2002; Zbl
    1077.68565)].
rv: