Generation of reduced certificates in abstraction-carrying code

Albert Albiol, Elvira; Arenas Sánchez, Purificación; Puebla Sánchez, Alvaro Germán y Hermenegildo, Manuel V. (2006). Generation of reduced certificates in abstraction-carrying code. En: "VI Jornadas Programación y Lenguajes (PROLE'06)", 4 al 6 de octubre, 2006, Sitges, Spain.

Descripción

Título: Generation of reduced certificates in abstraction-carrying code
Autor/es:
  • Albert Albiol, Elvira
  • Arenas Sánchez, Purificación
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: VI Jornadas Programación y Lenguajes (PROLE'06)
Fechas del Evento: 4 al 6 de octubre, 2006
Lugar del Evento: Sitges, Spain
Título del Libro: VI Jornadas Programación y Lenguajes (PROLE'06)
Fecha: 2006
Materias:
Palabras Clave Informales: Reduced certificates, abstraction-carrying code, abstract interpretation, mobile code safety, logic programming, certificados reducidos, interpretación de resúmenes, código con demostración, código móvil de seguridad, programación lógica.
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 (657kB) | Vista Previa

Resumen

Abstraction-Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certifícate and its generation is carried out automatically by a fixed-point analyzer. The advantage of providing a (fixedpoint) abstraction to the code consumer is that its validity is checked in a single pass of an abstract interpretation-based checker. A main challenge is to reduce the size of certificates as much as possible while at the same time not increasing checking time. In this paper, we first 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 certifícate in a single pass. Based on this notion, we then 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: 14607
Identificador DC: http://oa.upm.es/14607/
Identificador OAI: oai:oa.upm.es:14607
URL Oficial: http://congress.cimne.upc.es/prole/frontal/Aceptados.asp
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 07 Mar 2013 15:46
Ultima Modificación: 21 Abr 2016 14:20
  • 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