Internetware 2026
Sat 18 - Mon 20 July 2026 Gold Coast, Australia

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 Jul

Displayed 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
15m
Talk
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
15m
Talk
Feedback-Oriented Retrieval and Guided Editing for Java Meta-Decompilation
Research Track
Puhua Sun Zhejiang University, Xing Hu Zhejiang University, Xin Xia Zhejiang University
16:30
15m
Talk
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
15m
Talk
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
15m
Talk
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
15m
Talk
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