Program development using abstract interpretation (and the ciao system preprocessor)

Hermenegildo, Manuel V. and Puebla Sánchez, Alvaro Germán and Bueno Carrillo, Francisco and López García, Pedro (2003). Program development using abstract interpretation (and the ciao system preprocessor). In: "10th International Symposium, SAS 2003", June 11-13, 2003, San Diego, CA, USA. ISBN 9783540403258.


Title: Program development using abstract interpretation (and the ciao system preprocessor)
  • Hermenegildo, Manuel V.
  • Puebla Sánchez, Alvaro Germán
  • Bueno Carrillo, Francisco
  • López García, Pedro
Item Type: Presentation at Congress or Conference (Article)
Event Title: 10th International Symposium, SAS 2003
Event Dates: June 11-13, 2003
Event Location: San Diego, CA, USA
Title of Book: Static Analysis
Date: June 2003
ISBN: 9783540403258
Volume: 2694
Freetext Keywords: Program development, Global analysis, Abstract interpretation, Debugging, Verification, Partial evaluation, Program transformation, Optimization, Parallelization, Resource control, Programming environments, Multi-paradigm programming, (Constraint) Logic programming, Desarrollo de programas, Análisis global, Interpretación de resúmenes, Depuración, Verificación, Evolución parcial, Transformación de programas, Optimización, Paralelización, Control de recursos, Entornos de programación, Programación multi-paradigma, Programación lógica (restringida).
Faculty: Facultad de Informática (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[thumbnail of HERMENE_IPT_2003-2.pdf]
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview


The technique of Abstract Interpretation has allowed the development of very sophisticated global program analyses which are at the same time provably correct and practical. We present in a tutorial fashion a novel program development framework which uses abstract interpretation as a fundamental tool. The framework uses modular, incremental abstract interpretation to obtain information about the program. This information is used to validate programs, to detect bugs with respect to partial specifications written using assertions (in the program itself and/or in system librarles), to genérate and simplify run-time tests, and to perform high-level program transformations such as múltiple abstract specialization, parallelization, and resource usage control, all in a provably correct way. In the case of validation and debugging, the assertions can refer to a variety of program points such as procedure entry, procedure exit, points within procedures, or global computations. The system can reason with much richer information than, for example, traditional types. This includes data structure shape (including pointer sharing), bounds on data structure sizes, and other operational variable instantiation properties, as well as procedure-level properties such as determinacy, termination, non-failure, and bounds on resource consumption (time or space cost). CiaoPP, the preprocessor of the Ciao multi-paradigm programming system, which implements the described functionality, will be used to illustrate the fundamental ideas.

More information

Item ID: 14544
DC Identifier:
OAI Identifier:
Official URL:
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 23 Feb 2013 07:33
Last Modified: 27 Feb 2023 11:44
  • 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