Data-driven Recurrent Set Learning For Non-termination Analysis
Termination is a fundamental liveness property for program verification. In this paper, we revisit the problem of non-termination analysis and propose the first black-box learning algorithm for synthesizing recurrent sets, where the non-terminating samples are effectively speculated by a novel method. To ensure convergence of learning, we develop a learning algorithm which is guaranteed to converge to a valid recurrent set if one exists, and thus establish its relative completeness. The methods are implemented in a prototype tool and experimental results on public benchmarks show its efficacy in proving non-termination as it outperforms state-of-the-art tools, both in terms of cases solved and performance. Evaluation on non-linear programs also demonstrates its ability to handle complex programs.
Thu 18 MayDisplayed time zone: Hobart change
11:00 - 12:30 | Software verificationJournal-First Papers / NIER - New Ideas and Emerging Results / Technical Track / DEMO - Demonstrations at Meeting Room 106 Chair(s): Youcheng Sun The University of Manchester | ||
11:00 15mTalk | Data-driven Recurrent Set Learning For Non-termination Analysis Technical Track | ||
11:15 15mTalk | Compiling Parallel Symbolic Execution with Continuations Technical Track Guannan Wei Purdue University, Songlin Jia Purdue University, Ruiqi Gao Purdue University, Haotian Deng Purdue University, Shangyin Tan UC Berkeley, Oliver Bračevac Purdue University, Tiark Rompf Purdue University Pre-print | ||
11:30 15mTalk | Verifying Data Constraint Equivalence in FinTech Systems Technical Track Chengpeng Wang Hong Kong University of Science and Technology, Gang Fan Ant Group, Peisen Yao Zhejing University, Fuxiong Pan Ant Group, Charles Zhang Hong Kong University of Science and Technology Pre-print | ||
11:45 15mTalk | Tolerate Control-Flow Changes for Sound Data Race Prediction Technical Track Shihao Zhu State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,China, Yuqi Guo Institute of Software, Chinese Academy of Sciences, Beijing, China, Long Zhang Institute of Software, Chinese Academy of Sciences, Yan Cai Institute of Software at Chinese Academy of Sciences | ||
12:00 7mTalk | TSVD4J: Thread-Safety Violation Detection for Java DEMO - Demonstrations Shanto Rahman University of Texas at Austin, Chengpeng Li University of Texas at Austin, August Shi University of Texas at Austin | ||
12:07 7mTalk | What Petri Nets Oblige Us to Say Comparing Approaches for Behavior Composition Journal-First Papers Achiya Elyasaf Ben-Gurion University of the Negev, Tom Yaacov Ben-Gurion University of the Negev, Gera Weiss Ben-Gurion University of the Negev Link to publication DOI | ||
12:15 7mTalk | A Novel and Pragmatic Scenario Modeling Framework with Verification-in-the-loop for Autonomous Driving Systems NIER - New Ideas and Emerging Results Dehui Du East China Normal University, Bo Li East China Normal University, Chenghang Zheng East China Normal University |