Full text
Preview |
PDF
- Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview |
Bueno Carrillo, Francisco and Hermenegildo, Manuel V. and López García, Pedro and Puebla Sánchez, Alvaro Germán (2005). Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). "Science of computer programming", v. 58 (n. 1-2); pp. 115-140. ISSN 0167-6423. https://doi.org/10.1016/j.scico.2005.02.006.
Title: | Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor) |
---|---|
Author/s: |
|
Item Type: | Article |
Título de Revista/Publicación: | Science of computer programming |
Date: | 2005 |
ISSN: | 0167-6423 |
Volume: | 58 |
Subjects: | |
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, Depuración de programas, Verificación de programas, Evaluación parcial, Transformación de programas, Paralelización automática, Entornos de programas, Paradigma múltiple de programación, Programación lógica |
Faculty: | Facultad de Informática (UPM) |
Department: | Inteligencia Artificial |
Creative Commons Licenses: | Recognition - No derivative works - Non commercial |
Preview |
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 libraries), to generate and simplify run-time tests, and to perform high-level program transformations such as multiple 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, nonfailure, 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.
Item ID: | 11151 |
---|---|
DC Identifier: | https://oa.upm.es/11151/ |
OAI Identifier: | oai:oa.upm.es:11151 |
DOI: | 10.1016/j.scico.2005.02.006 |
Official URL: | http://www.journals.elsevier.com/science-of-comput... |
Deposited by: | Biblioteca Facultad de Informatica |
Deposited on: | 25 Sep 2012 06:48 |
Last Modified: | 03 Mar 2023 09:35 |