A Practical Type Analysis for Verification of Modular Prolog Programs

Pietrzak, Pawel and Correas Fernandez, Jesús and Puebla Sánchez, Alvaro Germán and Hermenegildo, Manuel V. (2008). A Practical Type Analysis for Verification of Modular Prolog Programs. In: "ACM SIGPLAN 2008 Workshop on Partial Evaluation and Program Manipulation , PEPM'08", 07/01/2008-08/01/2008, San Francisco, USA. ISBN 978-1-59593-977-7.

Description

Title: A Practical Type Analysis for Verification of Modular Prolog 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: ACM SIGPLAN 2008 Workshop on Partial Evaluation and Program Manipulation , PEPM'08
Event Dates: 07/01/2008-08/01/2008
Event Location: San Francisco, USA
Title of Book: Proceedings of the ACM SIGPLAN 2008 Symposium on Partial Evaluation and Semantics-Based Program Manipulation
Date: 2008
ISBN: 978-1-59593-977-7
Subjects:
Freetext Keywords: Program Analysis, Abstract Interpretation, Types, Verification, Modular Logic Programs, Logic Programming, Scalability
Faculty: Facultad de Informática (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[thumbnail of INVE_MEM_2008_60107.pdf]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (160kB) | Preview

Abstract

Regular types are a powerful tool for computing very precise descriptive types for logic programs. However, in the context of real life, modular Prolog programs, the accurate results obtained by regular types often come at the price of efficiency. In this paper we propose a combination of techniques aimed at improving analysis efficiency in this context. As a first technique we allow optionally reducing the accuracy of inferred types by using only the types defined by the user or present in the libraries. We claim that, for the purpose of verifying type signatures given in the form of assertions the precision obtained using this approach is sufficient, and show that analysis times can be reduced significantly. Our second technique is aimed at dealing with situations where we would like to limit the amount of reanalysis performed, especially for library modules. Borrowing some ideas from polymorphic type systems, we show how to solve the problem by admitting parameters in type specifications. This allows us to compose new call patterns with some pre computed analysis info without losing any information. We argue that together these two techniques contribute to the practical and scalable analysis and verification of types in Prolog programs.

More information

Item ID: 4373
DC Identifier: https://oa.upm.es/4373/
OAI Identifier: oai:oa.upm.es:4373
Official URL: http://www.program-transformation.org/PEPM08
Deposited by: Memoria Investigacion
Deposited on: 30 Sep 2010 08:16
Last Modified: 20 Apr 2016 13:37
  • 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