Abstraction-Carrying Code

10 years 11 months ago
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...
Elvira Albert, Germán Puebla, Manuel V. Her
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where LPAR
Authors Elvira Albert, Germán Puebla, Manuel V. Hermenegildo
Comments (0)