Abstract Interpretation-based verification/certification in the ciaoPP system

Puebla Sánchez, Alvaro Germán and Albert Albiol, Elvira and Hermenegildo, Manuel V. (2005). Abstract Interpretation-based verification/certification in the ciaoPP system. In: "MoVeLog'05 Mobile Code Safety and Program Verification Using Computational Logic Tools", Oct. 5, 2005, Sitges, Spain.

Description

Title: Abstract Interpretation-based verification/certification in the ciaoPP system
Author/s:
  • Puebla Sánchez, Alvaro Germán
  • Albert Albiol, Elvira
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: MoVeLog'05 Mobile Code Safety and Program Verification Using Computational Logic Tools
Event Dates: Oct. 5, 2005
Event Location: Sitges, Spain
Title of Book: Mobile Code Safety and Program Verification Using Computational Logic Tools (MoveLog'05)
Date: October 2005
Subjects:
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 (747kB) | Preview

Abstract

CiaoPP is the abstract interpretation-based preprocessor of the Ciao multi-paradigm (Constraint) Logic Programming system. It uses modular, incremental abstract interpretation as a fundamental tool to obtain information about programs. In CiaoPP, the semantic approximations thus produced have been applied to perform high- and low-level optimizations during program compilation, including transformations such as múltiple abstract specialization, parallelization, partial evaluation, resource usage control, and program verification. More recently, novel and promising applications of such semantic approximations are being applied in the more general context of program development such as program verification. In this work, we describe our extensión of the system to incorpórate Abstraction-Carrying Code (ACC), a novel approach to mobile code safety. ACC follows the standard strategy of associating safety certificates to programs, originally proposed in Proof Carrying- Code. A distinguishing feature of ACC is that 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 abstractinterpreter. We have implemented and benchmarked ACC within CiaoPP. The experimental results show that the checking phase is indeed faster than the proof generation phase, and that the sizes of certificates are reasonable. Moreover, the preprocessor is based on compile-time (and run-time) tools for the certification of CLP programs with resource consumption assurances.

More information

Item ID: 14538
DC Identifier: http://oa.upm.es/14538/
OAI Identifier: oai:oa.upm.es:14538
Official URL: http://babel.ls.fi.upm.es/movelog05/#Program
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 22 Feb 2013 07:29
Last Modified: 21 Apr 2016 14:15
  • 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