Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program TerminationVirtual
Mon 18 Oct 2021 22:35 - 22:50 at Zurich D - Verification / Theory (mirror) Chair(s): Yue Li
We propose an automated method for proving termination of $\pi$-calculus processes, based on a reduction to termination of sequential programs: we translate a $\pi$-calculus process to a sequential program, so that the termination of the latter implies that of the former. We can then use an off-the-shelf termination verification tool to check termination of the sequential program. Our approach has been partially inspired by Deng and Sangiorgi’s termination analysis for the $\pi$-calculus, and checks that there is no infinite chain of communications on replicated input channels, by converting such a chain of communications to a chain of recursive function calls in the target sequential program. We have implemented an automated tool based on the proposed method and confirmed its effectiveness.
Mon 18 OctDisplayed time zone: Central Time (US & Canada) change
13:50 - 15:10 | |||
13:50 15mTalk | Preprocessing of Alternating Automata for Language Emptiness TestingVirtual Research Papers Pavol Vargovčík Brno University of Technology, Czech Republic, Lukáš Holík Brno University of Technology | ||
14:05 15mTalk | Proving LTL Properties of Bitvector Programs and Decompiled BinariesVirtual Research Papers Cyrus Liu Stevens Institute of Technology, Chengbin Pang Stevens Institute of Technology, Daniel Dietsch University of Freiburg, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology, Georgios Portokalidis Stevens Institute of Technology, Jun Xu Stevens Institute of Technology | ||
14:20 15mTalk | Solving Not-Substring with Flat AbstractionVirtual Research Papers Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Yu-Fang Chen Academia Sinica, Taiwan, Bui Phi Diep Uppsala University, Sweden, Lukáš Holík Brno University of Technology, Denghang Hu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Wei-Lun Tsai Academia Sinica, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Di-De Yen Academia Sinica | ||
14:35 15mTalk | Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program TerminationVirtual Research Papers Tsubasa Shoshi The University of Tokyo, Takuma Ishikawa The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan | ||
14:50 20mLive Q&A | Q&A and discussionVirtual Research Papers |
21:50 - 23:10 | |||
21:50 15mTalk | Preprocessing of Alternating Automata for Language Emptiness TestingVirtual Research Papers Pavol Vargovčík Brno University of Technology, Czech Republic, Lukáš Holík Brno University of Technology | ||
22:05 15mTalk | Proving LTL Properties of Bitvector Programs and Decompiled BinariesVirtual Research Papers Cyrus Liu Stevens Institute of Technology, Chengbin Pang Stevens Institute of Technology, Daniel Dietsch University of Freiburg, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology, Georgios Portokalidis Stevens Institute of Technology, Jun Xu Stevens Institute of Technology | ||
22:20 15mTalk | Solving Not-Substring with Flat AbstractionVirtual Research Papers Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Yu-Fang Chen Academia Sinica, Taiwan, Bui Phi Diep Uppsala University, Sweden, Lukáš Holík Brno University of Technology, Denghang Hu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Wei-Lun Tsai Academia Sinica, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Di-De Yen Academia Sinica | ||
22:35 15mTalk | Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program TerminationVirtual Research Papers Tsubasa Shoshi The University of Tokyo, Takuma Ishikawa The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan | ||
22:50 20mLive Q&A | Q&A and discussionVirtual Research Papers |