Loop Invariant Inference through SMT Solving Enhanced Reinforcement Learning
Inferring loop invariants is one of the most challenging problems in program verification. It is highly desired to incorporate machine learning when inferring. This paper presents a Reinforcement Learning (RL) pruning framework to infer loop invariants over a general nonlinear hypothesis space. The key idea is to synergize the RL-based pruning and SMT solving to generate candidate invariants efficiently. To address the sparse reward problem in learning, we design a novel two-dimensional reward mechanism that enables the RL pruner to recognize the capability boundary of SMT solvers and learn the pruning heuristics in a few rounds. We have implemented our approach with Z3 SMT solver in the tool called LIPuS and conducted extensive experiments over the linear and nonlinear benchmarks. Experiment results show that LIPuS can solve the most cases compared to the state-of-the-art loop invariant inference tools such as Code2Inv, ICE-DT, GSpacer, SymInfer, ImplCheck, and Eldarica. Especially, LIPuS outperforms them significantly on nonlinear benchmarks.
Tue 18 JulDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 17:00 | ISSTA Online 2: Static AnalysisTechnical Papers at Habib Classroom (Gates G01) Chair(s): Julian Dolby IBM Research | ||
15:30 10mTalk | Fine-Grained Code Clone Detection with Block-Based Splitting of Abstract Syntax Tree Technical Papers Tiancheng Hu Huazhong University of Science and Technology, Zijing Xu Huazhong University of Science and Technology, Yilin Fang Huazhong University of Science and Technology, Yueming Wu Nanyang Technological University, Bin Yuan Huazhong University of Science and Technology, Deqing Zou Huazhong University of Science and Technology, Hai Jin Huazhong University of Science and Technology DOI | ||
15:40 10mTalk | Hybrid Inlining: A Framework for Compositional and Context-Sensitive Static Analysis Technical Papers Jiangchao Liu Ant Group; ByteDance, Jierui Liu Ant Group, Peng Di Ant Group, Diyu Wu Ant Group, Hengjie Zheng Ant Group, Alex X. Liu Ant Group, Jingling Xue UNSW DOI | ||
15:50 10mTalk | CGuard: Scalable and Precise Object Bounds Protection for C Technical Papers Piyus Kedia IIIT Delhi, Rahul Purandare University of Nebraska-Lincoln, Udit Kumar Agarwal University of British Columbia, Rishabh GGSIPU DOI | ||
16:00 10mTalk | Reducing the Memory Footprint of IFDS-Based Data-Flow Analyses using Fine-Grained Garbage CollectionACM SIGSOFT Distinguished Artifact Technical Papers DOI | ||
16:10 10mTalk | GenCoG: A DSL-Based Approach to Generating Computation Graphs for TVM Testing Technical Papers Zihan Wang Shanghai Jiao Tong University, Pengbo Nie Shanghai Jiao Tong University, Xinyuan Miao Shanghai Jiao Tong University, Yuting Chen Shanghai Jiao Tong University, Chengcheng Wan East China Normal University, Lei Bu Nanjing University, Jianjun Zhao Kyushu University DOI | ||
16:20 10mTalk | Splendor: Static Detection of Stored XSS in Modern Web Applications Technical Papers He Su Institute of Information Engineering at Chinese Academy of Sciences, Feng Li Institute of Information Engineering at Chinese Academy of Sciences, Lili Xu Institute of Information Engineering at Chinese Academy of Sciences, Wenbo Hu Institute of Information Engineering at Chinese Academy of Sciences, Yujie Sun Institute of Information Engineering at Chinese Academy of Sciences, Qing Sun Institute of Information Engineering at Chinese Academy of Sciences, Huina Chao Institute of Information Engineering at Chinese Academy of Sciences, Wei Huo Institute of Information Engineering at Chinese Academy of Sciences DOI | ||
16:30 10mTalk | Improving Bit-Blasting for Nonlinear Integer ConstraintsACM SIGSOFT Distinguished Paper Technical Papers 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, Pei Huang Stanford University, Minghao Liu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, 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 DOI | ||
16:40 10mTalk | Loop Invariant Inference through SMT Solving Enhanced Reinforcement Learning Technical Papers Shiwen Yu National University of Defense Technology, Ting Wang National University of Defense Technology, Ji Wang National University of Defense Technology DOI |