Generation of reduced certificates in abstraction-carrying code

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

Description

Title: Generation of reduced certificates in abstraction-carrying code
Author/s:
  • Albert Albiol, Elvira
  • Arenas Sánchez, Purificación
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: VI Jornadas Programación y Lenguajes (PROLE'06)
Event Dates: 4 al 6 de octubre, 2006
Event Location: Sitges, Spain
Title of Book: VI Jornadas Programación y Lenguajes (PROLE'06)
Date: 2006
Subjects:
Freetext Keywords: 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.
Faculty: Facultad de Informática (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (657kB) | Preview

Abstract

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.

More information

Item ID: 14607
DC Identifier: http://oa.upm.es/14607/
OAI Identifier: oai:oa.upm.es:14607
Official URL: http://congress.cimne.upc.es/prole/frontal/Aceptados.asp
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 07 Mar 2013 15:46
Last Modified: 21 Apr 2016 14:20
  • 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