Context-sensitive multivariant assertion checking in modular programs

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

Description

Title: Context-sensitive multivariant assertion checking in modular programs
Author/s:
  • Pietrzak, Pawel
  • Correas Fernandez, Jesús
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: 13th International Conference, LPAR 2006
Event Dates: November 13-17, 2006
Event Location: Phnom Penh, Cambodia
Title of Book: Logic for Programming, Artificial Intelligence, and Reasoning
Date: 2006
ISBN: 978-3-540-48281-9
Volume: 4246
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 (927kB) | Preview

Abstract

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.

More information

Item ID: 14338
DC Identifier: http://oa.upm.es/14338/
OAI Identifier: oai:oa.upm.es:14338
Official URL: http://link.springer.com/chapter/10.1007/11916277_27
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 22 Jan 2013 08:04
Last Modified: 21 Apr 2016 13:57
  • 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