Abstraction-carrying code

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


Título: Abstraction-carrying code
  • Albert Albiol, Elvira
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: 11th International Conference, LPAR 2004
Fechas del Evento: March 14-18, 2005
Lugar del Evento: Montevideo, Uruguay
Título del Libro: Logic for Programming, Artificial Intelligence, and Reasoning
Fecha: 2005
ISBN: 9783540252368
Volumen: 3452
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Inteligencia Artificial
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (1MB) | Vista Previa


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.

Más información

ID de Registro: 14364
Identificador DC: http://oa.upm.es/14364/
Identificador OAI: oai:oa.upm.es:14364
URL Oficial: http://link.springer.com/chapter/10.1007%2F978-3-540-32275-7_25?LI=true
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 27 Ene 2013 06:55
Ultima Modificación: 21 Abr 2016 13:59
  • GEO_UP4
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • InvestigaM
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM