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

Separation logic is successful for software verification in both theory and practice. Decision procedure for symbolic heaps is one of the key issues. This paper proposes a cyclic proof system for symbolic heaps with general form of inductive definitions called cone inductive definitions, and shows its soundness and completeness. Cone inductive definitions are obtained from bounded-treewidth inductive definitions by imposing some restrictions for existentials, but they still include a wide class of recursive data structures. The completeness is proved by using a proof search algorithm and it also gives us a decision procedure for entailments of symbolic heaps with cone inductive definitions. The time complexity of the algorithm is nondeterministic double exponential. A prototype system for the algorithm is implemented and experimental results are also presented.

Tue 3 Dec
Times are displayed in time zone: (GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi change

15:30 - 17:15: Research Papers - Verification at Bali Room
Chair(s): Zhilin WuState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
aplas-2019-papers15:30 - 15:45
Yu-Fang ChenAcademia Sinica, Chang-Yi ChiangGraduate Institute of Information Management, National Taipei University, Taiwan, Lukáš HolíkBrno University of Technology, Wei-Tsung KaoInstitute of Information Science, Academia Sinica, Taiwan, Hsin-Hung LinInstitute of Information Science, Academia Sinica, Taiwan, Yean-Fu WenGraduate Institute of Information Management, National Taipei University, Taiwan, Tomas VojnarBrno University of Technology, Wei-Cheng WuInstitute of Information Science, Academia Sinica, Taiwan
aplas-2019-papers15:45 - 16:15
Wenbo Zhang, Huan LongShanghai Jiao Tong University, Xian XuEast China University of Science and Technology
aplas-2019-papers16:15 - 16:45
Makoto TatsutaNational Institute of Informatics, Koji NakazawaGraduate School of Informatics, Nagoya University, Daisuke KimuraToho University
aplas-2019-papers16:45 - 17:15
Long H. PhamSingapore University of Technology and Design, Jun SunSingapore Management University, Singapore, Quang Loc LeTeesside University