Tue 18 Jul 2023 16:30 - 16:40 at Habib Classroom (Gates G01) - ISSTA Online 2: Static Analysis Chair(s): Julian Dolby

Nonlinear integer constraints are common and difficult in the verification and analysis of software/hardware. SMT(QF_NIA) generalizes such constraints, which is a boolean combination of nonlinear integer arithmetic constraints. A classical method to solve SMT(QF_NIA) is bit-blasting, which reduces them to boolean satisfiability problems. Currently, the existing pure bit-blasting based solvers are noncompetitive with other state-of-the-art SMT solvers. The bit-blasting based methods have some problems: First, the bit-blasting method is hampered by nonlinear multiplication operations; second, it sometimes does not search in a proper search space; and third, it contains some redundancy.

In this paper, we focus on improving the efficiency of bit-blasting based method. To decide on a proper search space, we proposed an adaptive function for hard nonlinear multiplications, and heuristic strategies to analyze specific constraints. We also found that different orders in successive additions will result in bit vectors with different bit-widths. We proposed an optimal order decision algorithm to save redundancy in successive additions. We implement a solver with the proposed methods named BLAN. Experiments demonstrate that BLAN outperforms other state-of-the-art SMT solvers (APROVE, CVC5, MATHSAT, YICES2, Z3) on the satisfiable SMT(QF_NIA) instances in SMT-LIB. We provide an outlook of BLAN on solving unsatisfiable instances via combining with other solvers. Sensitivity analysis also demonstrates the effectiveness of the proposed methods.

Tue 18 Jul

Displayed 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
10m
Talk
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
10m
Talk
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
10m
Talk
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
10m
Talk
Reducing the Memory Footprint of IFDS-Based Data-Flow Analyses using Fine-Grained Garbage CollectionACM SIGSOFT Distinguished Artifact
Technical Papers
Dongjie He UNSW, Yujiang Gui UNSW, Yaoqing Gao Huawei Toronto Research Center, Jingling Xue UNSW
DOI
16:10
10m
Talk
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
10m
Talk
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
10m
Talk
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
10m
Talk
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