Abstract Interpretation-based verification/certification in the ciaoPP system

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

Descripción

Título: Abstract Interpretation-based verification/certification in the ciaoPP system
Autor/es:
  • Puebla Sánchez, Alvaro Germán
  • Albert Albiol, Elvira
  • Hermenegildo, Manuel V.
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: MoVeLog'05 Mobile Code Safety and Program Verification Using Computational Logic Tools
Fechas del Evento: Oct. 5, 2005
Lugar del Evento: Sitges, Spain
Título del Libro: Mobile Code Safety and Program Verification Using Computational Logic Tools (MoveLog'05)
Fecha: Octubre 2005
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 (747kB) | Vista Previa

Resumen

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.

Más información

ID de Registro: 14538
Identificador DC: http://oa.upm.es/14538/
Identificador OAI: oai:oa.upm.es:14538
URL Oficial: http://babel.ls.fi.upm.es/movelog05/#Program
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 22 Feb 2013 07:29
Ultima Modificación: 21 Abr 2016 14:15
  • 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