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

Rust is an emerging programming language with superior security reliability. Its safety is guaranteed by both sophisticated validations in compile time and comprehensive safety checks at runtime. Beyond safety mechanisms, Rust provides a critical keyword \texttt{unsafe}, allowing users to perform more efficient low-level memory operations while bypassing partial safety constraints. In practice, Rust provides many standard library APIs as safe/unsafe counterparts that share the same underlying safety conditions. The safe versions include runtime safety checks to ensure that arguments satisfy the required safety conditions, while the unsafe versions invoke unsafe primitives and rely on external safety guarantees. Therefore, unsafe implementations are more flexible, but also introduce greater safety risks. We compare the behavioral differences between all paired safe/unsafe counterpart implementations in the Rust standard library, and abstract their safety conditions. According to their requirements, the safety conditions of some safe API calls in real programs may already guaranteed to hold, making the corresponding runtime checks redundant. In this paper, we propose an approach based on abstract interpretation to efficiently detect such safe APIs calls and replace them with their unsafe counterparts to eliminate redundant runtime checks. The proposed approach is evaluated on real-world Rust crates, comparing performance before and after the safe-to-unsafe replacements. Experimental results indicate that after the safe replacement of all identified program sites, the substituted operators can achieve speedups of up to $36$%.

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