Program development using Abstract Interpretation (and the Ciao system preprocessor)

被引:0
|
作者
Hermenegildo, MV [1 ]
Puebla, G
Bueno, F
López-García, P
机构
[1] Tech Univ Madrid, Dept Comp Sci, Madrid, Spain
[2] Univ New Mexico, Dept Comp Sci, Albuquerque, NM 87131 USA
[3] Univ New Mexico, Dept Elect & Comp Engn, Albuquerque, NM 87131 USA
来源
STATIC ANALYSIS, PROCEEDINGS | 2003年 / 2694卷
关键词
program development; global analysis; Abstract Interpretation; debugging; verification; partial evaluation; program transformation; optimization; parallelization; resource control; programming environments; multi-paradigm programming; (constraint) logic programming;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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, 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.
引用
收藏
页码:127 / 152
页数:26
相关论文
共 50 条
  • [1] Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
    Hermenegildo, MV
    Puebla, G
    Bueno, F
    López-García, P
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2005, 58 (1-2) : 115 - 140
  • [2] Program analysis, debugging, and optimization using the Ciao system preprocessor
    Hermenegildo, MV
    Bueno, F
    Puebla, G
    López, P
    [J]. LOGIC PROGRAMMING: PROCEEDINGS OF THE 1999 INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING, 1999, : 54 - 66
  • [3] DEEP LOGIC PROGRAM TRANSFORMATION USING ABSTRACT INTERPRETATION
    BOULANGER, DY
    [J]. LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1992, 592 : 79 - 101
  • [4] Using Fuzzing to Help Abstract Interpretation ased Program Verification
    Huang, Renjie
    Yin, Banghu
    Chen, Liqian
    [J]. 2022 IEEE 22ND INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY, AND SECURITY COMPANION, QRS-C, 2022, : 782 - 783
  • [5] Abstract Program Slicing: An Abstract Interpretation-Based Approach to Program Slicing
    Mastroeni, Isabella
    Zanardini, Damiano
    [J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2017, 18 (01)
  • [6] Program analysis: The abstract interpretation perspective
    Cousot, P
    [J]. ACM SIGPLAN NOTICES, 1997, 32 (01) : 73 - 76
  • [7] Program specialisation and abstract interpretation reconciled
    Leuschel, M
    [J]. LOGIC PROGRAMMING - PROCEEDINGS OF THE 1998 JOINT INTERNATIONAL CONFERENCE AND SYMPOSIUM ON LOGIC PROGRAMMING, 1998, : 220 - 234
  • [8] Infer Precise Program Invariant Using Abstract Interpretation with Recurrence Solving
    Fang, Zhenpeng
    Zhao, Xibin
    Zhou, Min
    [J]. 2017 IEEE 41ST ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1, 2017, : 196 - 201
  • [9] Capitalizing software development skills using CBR: The CIAO-SI system
    Nkambou, R
    [J]. INNOVATIONS IN APPLIED ARTIFICIAL INTELLIGENCE, 2004, 3029 : 483 - 491
  • [10] Optimal Program Synthesis via Abstract Interpretation
    Mell, Stephen
    Zdancewic, Steve
    Bastani, Osbert
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (POPL):