Write a Blog >>
APLAS 2020
Mon 30 November - Wed 2 December 2020
Mon 30 Nov 2020 16:00 - 16:30 at online - Debugging, Profiling and Constraint Solving Chair(s): Tachio Terauchi

Case split is a core proof rule in current decision procedures for the theory of string constraints. Its use is the primary cause of the state space explosion in string constraint solving, since it is the only rule that creates branches in the proof tree. Moreover, explicit handling of the case split rule may cause recomputation of the same tasks in multiple branches of the proof tree. In this paper, we propose a symbolic algorithm that significantly reduces such a redundancy. In particular, we encode a string constraint as a regular language and proof rules as rational transducers. This allows to perform similar steps in the proof tree only once, alleviating the state space explosion. In our preliminary experimental results, we validated that our technique (implemented in a Python prototype) works in many practical cases where other state-of-the-art solvers, such as CVC4 or Z3 fail to provide an answer.

Mon 30 Nov

Displayed time zone: Osaka, Sapporo, Tokyo change

15:30 - 17:00
Debugging, Profiling and Constraint SolvingResearch Papers at online
Chair(s): Tachio Terauchi Waseda University
15:30
30m
Talk
A Counterexample-Guided Debugger for Non-Recursive Datalog
Research Papers
Van-Dang Tran National Institute of Informatics, Japan, Hiroyuki Kato National Institute of Informatics, Japan, Zhenjiang Hu Peking University
16:00
30m
Talk
A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving
Research Papers
Yu-Fang Chen Academia Sinica, Taiwan, Vojtěch Havlena Brno University of Technology, Ondřej Lengál Brno University of Technology, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
16:30
30m
Talk
P3: A Profiler Suite for Parallel Applications on the Java Virtual Machine (Tool Paper)
Research Papers
Andrea Rosà University of Lugano, Switzerland, Walter Binder University of Lugano, Switzerland