Write a Blog >>

Modern programs are usually heap-based, where the programs manipulate heap-based data structures to perform computations. In software engineering tasks such as test generation and bounded verification, we need to determine the existence of a reachable heap state that satisfies a given specification, or construct the heap state by a sequence of calls to the public methods. Given the huge space combined from the methods and their arguments, the existing approaches typically adopt static analysis or heuristic search to explore only a small part of search space in the hope of finding the target state and target call sequence early on. However, these approaches do not have satisfactory performance on many real-world complex methods and specifications. In this paper, we propose an efficient synthesis algorithm for method call sequences, including an offline procedure for exploring all reachable heap states within a scope, and an online procedure for generating a method call sequence from the explored heap states to satisfy the given specification. To improve the efficiency of state exploration, we introduce a notion of abstract heap state for compactly representing heap states of the same structure and propose a strategy of merging structurally-isomorphic states. The experimental results demonstrate that our approach substantially outperforms the baselines in both test generation and bounded verification.

Wed 12 Oct

Displayed time zone: Eastern Time (US & Canada) change

16:00 - 18:00
Technical Session 19 - Formal Methods and Models IResearch Papers / Journal-first Papers / Tool Demonstrations at Ballroom C East
Chair(s): Michalis Famelis Université de Montréal
16:00
20m
Research paper
Automatic Comment Generation via Multi-Pass Deliberation
Research Papers
Fangwen Mu Institute of Software Chinese Academy of Sciences, Xiao Chen Institute of Software Chinese Academy of Sciences, Lin Shi ISCAS, Song Wang York University, Qing Wang Institute of Software at Chinese Academy of Sciences
16:20
10m
Demonstration
Building recommender systems for modelling languages with DroidVirtual
Tool Demonstrations
Lissette Almonte Universidad Autónoma de Madrid, Esther Guerra Universidad Autónoma de Madrid, Iván Cantador Universidad Autónoma de Madrid, Juan de Lara Autonomous University of Madrid
Pre-print Media Attached
16:30
10m
Demonstration
RobSimVer: A Tool for RoboSim Modeling and AnalysisVirtual
Tool Demonstrations
Dehui Du East China Normal University, Ana Cavalcanti University of York, JihuiNie East China Normal University
16:40
20m
Research paper
Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural NetworksVirtual
Research Papers
Zhaodi Zhang East China Normal University, Yiting Wu East China Normal University, Si Liu ETH Zurich, Jing Liu East China Normal University, Min Zhang East China Normal University
17:00
20m
Research paper
Efficient Synthesis of Method Call Sequences for Test Generation and Bounded VerificationVirtual
Research Papers
Yunfan Zhang Peking University, Ruidong Zhu Peking University, Yingfei Xiong Peking University, Tao Xie Peking University
17:20
20m
Paper
Demystifying Performance Regressions in String SolversVirtual
Journal-first Papers
Yao Zhang , Xiaofei Xie Singapore Management University, Singapore, Yi Li Nanyang Technological University, Yun Lin National University of Singapore, Sen Chen Tianjin University, Yang Liu Nanyang Technological University, Xiaohong Li TianJin University
Link to publication DOI
17:40
20m
Research paper
Detecting Semantic Code Clones by Building AST-based Markov Chains ModelVirtual
Research Papers
Yueming Wu Nanyang Technological University, Siyue Feng Huazhong University of Science and Technology, Deqing Zou Huazhong University of Science and Technology, Hai Jin Huazhong University of Science and Technology