A Practical Type Analysis for Verification of Modular Prolog Programs

Pietrzak, Pawel; Correas Fernandez, Jesús; Puebla Sánchez, Alvaro Germán y Hermenegildo, Manuel V. (2008). A Practical Type Analysis for Verification of Modular Prolog Programs. En: "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.

Descripción

Título: A Practical Type Analysis for Verification of Modular Prolog 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: ACM SIGPLAN 2008 Workshop on Partial Evaluation and Program Manipulation , PEPM'08
Fechas del Evento: 07/01/2008-08/01/2008
Lugar del Evento: San Francisco, USA
Título del Libro: Proceedings of the ACM SIGPLAN 2008 Symposium on Partial Evaluation and Semantics-Based Program Manipulation
Fecha: 2008
ISBN: 978-1-59593-977-7
Materias:
Palabras Clave Informales: Program Analysis, Abstract Interpretation, Types, Verification, Modular Logic Programs, Logic Programming, Scalability
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Lenguajes y Sistemas Informáticos e Ingeniería del Software
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 (160kB) | Vista Previa

Resumen

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.

Más información

ID de Registro: 4373
Identificador DC: http://oa.upm.es/4373/
Identificador OAI: oai:oa.upm.es:4373
URL Oficial: http://www.program-transformation.org/PEPM08
Depositado por: Memoria Investigacion
Depositado el: 30 Sep 2010 08:16
Ultima Modificación: 20 Abr 2016 13:37
  • 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