Abstraction-Carrying Code

ion-Carrying Code Elvira Albert1 , Germ´an Puebla2 , and Manuel Hermenegildo2,3 1 DSIP, Universidad Complutense Madrid 2 Facultad de Inform´atica, Technical University of Madrid 3 Depts. of Comp. Sci. and El. and Comp. Eng., U. of New Mexico Abstract. Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The practical uptake of PCC greatly depends on the existence of a variety of enabling technologies which allow both to prove programs correct and to replace a costly verification process by an efficient checking procedure on the consumer side. In this work we propose AbstractionCarrying Code (ACC), a novel approach which uses abstract interpretation as enabling technology. We argue that the large body of applicaabstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class y policies which can be defined over different abstract doma...

• Type: Conference
• Year: 2004
• Where: LPAR
• Authors: Elvira Albert, Germán Puebla, Manuel V. Hermenegildo
• Keywords: Abstract Interpretation, Code, LPAR 2004, Mobile Code Safety