On abstraction-carrying code and certificate-size reduction

Puebla Sánchez, Alvaro Germán; Albert Albiol, Elvira; Arenas Sánchez, Purificación y Hermenegildo, Manuel V. (2006). On abstraction-carrying code and certificate-size reduction. En: "EAAI 2006 1st International Workshop on Emerging Applications of Abstract Interpretation", March 26th, 2006, Vienna, Austria.

Descripción

Título: On abstraction-carrying code and certificate-size reduction
Autor/es:
  • Puebla Sánchez, Alvaro Germán
  • Albert Albiol, Elvira
  • Arenas Sánchez, Purificación
  • Hermenegildo, Manuel V.
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: EAAI 2006 1st International Workshop on Emerging Applications of Abstract Interpretation
Fechas del Evento: March 26th, 2006
Lugar del Evento: Vienna, Austria
Título del Libro: Electronic Notes in Theoretical Computer Science
Fecha: Marzo 2006
Materias:
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Inteligencia Artificial
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (935kB) | Vista Previa

Resumen

Abstraction-Carrying Code (ACC) is a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certificate and its generation is carried out automatically by a fixed-point analyzer. The advantage of providing a (fixed-point) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible, while at the same time not increasing checking time. Intuitively, we only include in the certificate the information which the checker is unable to reproduce without iterating. We introduce the notion of reduced certifícate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certificate in a single pass. Based on this notion, we show how to instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker.

Más información

ID de Registro: 14523
Identificador DC: http://oa.upm.es/14523/
Identificador OAI: oai:oa.upm.es:14523
URL Oficial: http://www.elsevier.com/journals/electronic-notes-in-theoretical-computer-science/1571-0661#
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 21 Feb 2013 08:59
Ultima Modificación: 21 Abr 2016 14:14
  • 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
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM