Context-sensitive multivariant assertion checking in modular programs

Pietrzak, Pawel; Correas Fernandez, Jesús; Puebla Sánchez, Alvaro Germán y Hermenegildo, Manuel V. (2006). Context-sensitive multivariant assertion checking in modular programs. En: "13th International Conference, LPAR 2006", November 13-17, 2006, Phnom Penh, Cambodia. ISBN 978-3-540-48281-9.

Descripción

Título: Context-sensitive multivariant assertion checking in modular programs
Autor/es:
  • Pietrzak, Pawel
  • Correas Fernandez, Jesús
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: 13th International Conference, LPAR 2006
Fechas del Evento: November 13-17, 2006
Lugar del Evento: Phnom Penh, Cambodia
Título del Libro: Logic for Programming, Artificial Intelligence, and Reasoning
Fecha: 2006
ISBN: 978-3-540-48281-9
Volumen: 4246
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 (927kB) | Vista Previa

Resumen

We propose a modular, assertion-based system for verification and debugging of large logic programs, together with several interesting models for checking assertions statically in modular programs, each with different characteristics and representing different trade-offs. Our proposal is a modular and multivariant extensión of our previously proposed abstract assertion checking model and we also report on its implementation in the CiaoPP system. In our approach, the specification of the program, given by a set of assertions, may be partial, instead of the complete specification required by raditional verification systems. Also, the system can deal with properties which cannot always be determined at compile-time. As a result, the proposed system needs to work with safe approximations: all assertions proved correct are guaranteed to be valid and all errors actual errors. The use of modular, context-sensitive static analyzers also allows us to introduce a new distinction between assertions checked in a particular context or checked in general.

Más información

ID de Registro: 14338
Identificador DC: http://oa.upm.es/14338/
Identificador OAI: oai:oa.upm.es:14338
URL Oficial: http://link.springer.com/chapter/10.1007/11916277_27
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 22 Ene 2013 08:04
Ultima Modificación: 21 Abr 2016 13:57
  • 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