Value Analysis of Floating-Point Fortran Programs by Combining Interval and Zonotopic Abstractions
In the field of scientific computing, Fortran programs contain extensive numerical operations based on the finite precision representation of floating-point numbers, making them prone to potential runtime errors, such as arithmetic overflow, division by zero, etc. The key to check for those runtime errors is to infer value ranges of floating-point variables and expressions. In this paper, we propose to conduct value analysis of floating-point programs by combining interval and zonotopic abstractions. First, we introduce a lightweight zonotopic abstraction for floating-point programs, which soundly handles floating-point arithmetic operations but without introducing too many noise terms. On particular, we present a boundary search based algorithm to improve the division operation of the classic zonotopic abstraction. On this basis, we propose to combine interval and zonotopic abstractions to improve the analysis precision. Finally, we developed a static analyzer based on the above approach for floating-point Fortran programs. Experimental results demonstrate that the proposed method enhances the value analysis efficiency of floating-point Fortran programs while maintaining soundness.
| Value Analysis of Floating-Point Fortran Programs by Combining Interval and Zonotopic Abstractions (InternetWare2026 -Value Analysis of Floating-Point Fortran Programs by Combining Interval and Zonotopic Abstractions.pdf) | 676KiB |
Sat 18 JulDisplayed time zone: Brisbane change
16:00 - 17:30 | Session 5: Program Analysis, Verification, and Code TransformationResearch Track / New Idea at Ballroom Chair(s): Zihan Wang The University of Queensland and CSIRO's Data61 | ||
16:00 15mTalk | Bypassing Redundant Safety Checks in Rust via Static Analysis Research Track Yunlong Yu Shandong University, Qingdan Meng Shandong University, Wei Zhang Shandong University, Lei Ju Shandong University | ||
16:15 15mTalk | Feedback-Oriented Retrieval and Guided Editing for Java Meta-Decompilation Research Track | ||
16:30 15mTalk | Value Analysis of Floating-Point Fortran Programs by Combining Interval and Zonotopic Abstractions Research Track Dengping Wei National University of Defense Technology, Banghu Yin College of Computer, National University of Defense Technology, Changsha, China, Yi Huang National University of Defense Technology, Liqian Chen National University of Defense Technology File Attached | ||
16:45 15mTalk | Editor Specialization: Deriving DSL Editors through Editing Service Lifting Research Track Ziheng Wang Peking University, Zhichao Guan Peking University, Xiaoyang Lu Purdue University, Di Wang Peking University, Hongjie Chen Peking University, Zhenjiang Hu Peking University File Attached | ||
17:00 15mTalk | Predicates with One Hole for Linked Data Structures in Separation Logic Research Track Xingpeng Liu National University of Defense Technology, Yanjun Wen National University of Defense Technology, Hengzhu Liu National University of Defense Technology, Ji Wang National University of Defense Technology | ||
17:15 15mTalk | ACSLAgent: Generation and Synthesis of Formal Specifications for C programs via LLM-based Agent New Idea Lezhi Ma Nanjing University, Han Wang Nanjing University, Shangqing Liu Nanjing University, Lei Bu Nanjing University | ||