Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions
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 DecDisplayed 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 15mTalk | 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 30mTalk | 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 30mTalk | 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 30mTalk | 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 | ||