ASE 2023
Mon 11 - Fri 15 September 2023 Kirchberg, Luxembourg
Wed 13 Sep 2023 14:06 - 14:18 at Room C - Program Verification 1 Chair(s): Nico Rosner

Detecting non-termination is crucial for ensuring program correctness and security, such as preventing denial-of-service attacks. While termination analysis has been studied for many years, existing methods have limited scalability and are only effective on small programs. To address this issue, we propose a practical termination checking technique, called EndWatch, for detecting non-termination through testing. Specifically, we introduce two methods to generate non-termination oracles based on checking state revisits, i.e., if the program returns to a previously visited state at the same program location, it does not terminate. The non-termination oracles can be incorporated into testing tools (e.g., AFL used in this paper) to detect non-termination in large programs. For linear loops, we perform symbolic execution on individual loops to infer State Revisit Conditions (SRC) and instrument SRC into target loops. For non-linear loops, we instrument target loops for checking concrete state revisits during execution. We evaluated EndWatch on standard benchmarks with small-sized programs and real-world projects with large-sized programs. The evaluation results show that EndWatch is more effective than the state-of-the-art tools on standard benchmarks (detecting 87% of non-terminating programs while the best baseline detects only 67%), and useful in detecting non-termination in real-world projects (detecting 90% of known non-termination CVEs and 4 unknown bugs).

EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software (Loop-nonterm-v8.pdf)1.11MiB

Wed 13 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Program Verification 1Research Papers / NIER Track / Tool Demonstrations at Room C
Chair(s): Nico Rosner Amazon Web Services
13:30
12m
Talk
CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification
Tool Demonstrations
Dirk Beyer LMU Munich, Po-Chun Chien LMU Munich, Nian-Ze Lee LMU Munich
Pre-print Media Attached File Attached
13:42
12m
Talk
Demystifying Template-based Invariant Generation for Bit-Vector Programs
Research Papers
Peisen Yao Zhejing University, Jingyu Ke Shanghai Jiao Tong University, Jiahui Sun Zhejiang University, Hongfei Fu Shanghai Jiao Tong University, Rongxin Wu Xiamen University, Kui Ren Zhejiang University
13:54
12m
Talk
PSMT: Satisfiability Modulo Theories Meets Probability Distribution
NIER Track
Fuqi Jia Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Rui Han Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Xutong Ma State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China, Baoquan Cui Institute of Software at Chinese Academy of Sciences, China, Minghao Liu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Pei Huang Stanford University, Feifei Ma Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Jian Zhang Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
Pre-print File Attached
14:06
12m
Talk
EndWatch: A Practical Method for Detecting Non-Termination in Real-World SoftwareACM Distinguished Paper
Research Papers
Yao Zhang Tianjin University, Xiaofei Xie Singapore Management University, Yi Li Nanyang Technological University, Sen Chen Tianjin University, Cen Zhang Nanyang Technological University, Xiaohong Li Tianjin University
Pre-print File Attached
14:18
12m
Talk
Symbolic Fixpoint Algorithms for Logical LTL Games
Research Papers
Stanly Samuel Indian Institute of Science, India, Deepak D'Souza IISc Bangalore, Raghavan Komondoor Indian Institute of Science, India
Pre-print Media Attached File Attached
14:30
12m
Talk
SAT-verifiable LTL Satisfiability Checking via Graph Representation LearningRecorded talk
NIER Track
Weilin Luo Sun Yat-Sen University, Yuhang Zheng Sun Yat-Sen University, Rongzhen Ye Sun Yat-Sen University, Hai Wan School of Data and Computer Science, Sun Yat-sen University, Jianfeng Du Guangdong University of Foreign Studies, Pingjia Liang Sun Yat-Sen University, Polong Chen Sun Yat-Sen University
Media Attached