Abstraction-carrying code

Albert Albiol, Elvira and Puebla Sánchez, Alvaro Germán and Hermenegildo, Manuel V. (2005). Abstraction-carrying code. In: "11th International Conference, LPAR 2004", March 14-18, 2005, Montevideo, Uruguay. ISBN 9783540252368.


Title: Abstraction-carrying code
  • Albert Albiol, Elvira
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: 11th International Conference, LPAR 2004
Event Dates: March 14-18, 2005
Event Location: Montevideo, Uruguay
Title of Book: Logic for Programming, Artificial Intelligence, and Reasoning
Date: 2005
ISBN: 9783540252368
Volume: 3452
Faculty: Facultad de Informática (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[thumbnail of HERME_ARC_2005-5.pdf]
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview


Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certifícate (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 efñcient checking procedure on the consumer side. In this work we propose Abstraction-Carrying Code (ACC), a novel approach which uses abstract interpretation as enabling technology. We argüe that the large body of applications of abstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class of safety policies which can be defined over different abstract domains. We use an abstraction (or abstract model) of the program computed by standard static analyzers as a certifícate. The validity of the abstraction on the consumer side is checked in a single-pass by a very efficient and specialized abstract-interpreter. We believe that ACC brings the expressiveness, flexibility and automation which is inherent in abstract interpretation techniques to the área of mobile code safety. We have implemented and benchmarked ACC within the Ciao system preprocessor. The experimental results show that the checking phase is indeed faster than the proof generation phase, and that the sizes of certificates are reasonable.

More information

Item ID: 14364
DC Identifier: https://oa.upm.es/14364/
OAI Identifier: oai:oa.upm.es:14364
Official URL: http://link.springer.com/chapter/10.1007%2F978-3-5...
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 27 Jan 2013 06:55
Last Modified: 27 Feb 2023 12:33
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM