Write a Blog >>
APLAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Mon 18 Oct 2021 14:20 - 14:35 at Zurich D - Verification / Theory Chair(s): Xiaokang Qiu
Mon 18 Oct 2021 22:20 - 22:35 at Zurich D - Verification / Theory (mirror) Chair(s): Yue Li

Not-substring is currently among the least supported types of string constraints, and existing solvers use only relatively crude heuristics. Yet, not-substring occurs relatively often in practical examples and is useful in encoding other types of constraints. In this paper, we propose a systematic way to solve not-substring using the Counter-Example Guided Abstraction Refinement (CEGAR) framework based on flat abstraction. In such a framework, the domain of string variables is restricted to flat languages and subsequently, the whole constraints can be expressed as linear arithmetic formulae. We show that non-substring constraints can be flattened efficiently, and provide experimental evidence that the proposed solution for not-substring is competitive with the state-of-the-art string solvers.

Mon 18 Oct

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

13:50 - 15:10
Verification / TheoryResearch Papers at Zurich D +8h
Chair(s): Xiaokang Qiu Purdue University, USA
13:50
15m
Talk
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
15m
Talk
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
15m
Talk
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
15m
Talk
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
20m
Live Q&A
Q&A and discussionVirtual
Research Papers

21:50 - 23:10
Verification / Theory (mirror)Research Papers at Zurich D
Chair(s): Yue Li Nanjing University
21:50
15m
Talk
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
15m
Talk
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
15m
Talk
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
15m
Talk
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
20m
Live Q&A
Q&A and discussionVirtual
Research Papers