Write a Blog >>
APLAS 2019
Sun 1 - Wed 4 December 2019 Bali, Indonesia
Tue 3 Dec 2019 16:45 - 17:15 at Bali Room - Verification Chair(s): Zhilin Wu

Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, existing verifiers for heap-manipulating programs require user-provided specification for each function in the program in order to decompose the verification problem. The requirement, however, often hinders the users from applying such tools. To overcome the issue, we propose to automatically learn heap-related program invariants in a property-guided way for each function call. The invariants are learned based on the memory graphs observed during test execution and improved through memory graph mutation. We implemented a prototype of our approach and integrated it with two existing program verifiers. The experimental results show that our approach enhances existing verifiers effectively in automatically verifying complex heap-manipulating programs with multiple function calls.

Tue 3 Dec

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

15:30 - 17:15
VerificationResearch Papers at Bali Room
Chair(s): Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
15:30
15m
Talk
J-ReCoVer: Java Reducer Commutativity Verifier [Tool Paper]
Research Papers
Yu-Fang Chen Academia Sinica, Chang-Yi Chiang Graduate Institute of Information Management, National Taipei University, Taiwan, Lukáš Holík Brno University of Technology, Wei-Tsung Kao Institute of Information Science, Academia Sinica, Taiwan, Hsin-Hung Lin Institute of Information Science, Academia Sinica, Taiwan, Yean-Fu Wen Graduate Institute of Information Management, National Taipei University, Taiwan, Tomáš Vojnar Brno University of Technology, Wei-Cheng Wu Institute of Information Science, Academia Sinica, Taiwan
15:45
30m
Talk
Uniform Random Process Model Revisited
Research Papers
Wenbo Zhang , Huan Long Shanghai Jiao Tong University, Xian Xu East China University of Science and Technology
16:15
30m
Talk
Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions
Research Papers
Makoto Tatsuta National Institute of Informatics, Koji Nakazawa Graduate School of Informatics, Nagoya University, Daisuke Kimura Toho University
16:45
30m
Talk
Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning
Research Papers
Long H. Pham Singapore University of Technology and Design, Jun Sun Singapore Management University, Singapore, Quang Loc Le Teesside University