SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Tue 6 Dec 2022 16:00 - 16:30 at Lecture Theatre 2 - APLAS Papers Chair(s): Joxan Jaffar

Kobayashi et al.\ have recently shown that various verification problems for higher-order functional programs can naturally be reduced to the validity checking problem for $\text{HFL}\mathbb{Z}$, a higher-order fixpoint logic extended with integers. We propose a refinement type system for checking the validity of $\nu\text{HFL}\mathbb{Z}$ formulas, where $\nu\text{HFL}\mathbb{Z}$ is a fragment of $\text{HFL}\mathbb{Z}$ without least fixpoint operators, but sufficiently expressive for encoding safety property verification problems. Our type system has been inspired by the type system of Burn et al. for solving the satisfiability problem for HoCHC, which is essentially equivalent to the $\nu\text{HFL}\mathbb{Z}$ validity checking problem. Our type system is more expressive, however, due to a more sophisticated subtyping relation. We have implemented a type-based $\nu\text{HFL}\mathbb{Z}$ validity checker ${\rm R{\small e}THFL}$ based on the proposed type system, and confirmed through experiments that ${\rm R{\small e}THFL}$ can solve more instances than Horus, the tool based on Burn et al.’s type system.

#### Tue 6 DecDisplayed time zone: Auckland, Wellington change

 15:30 - 17:30 APLAS PapersCOVID Time Papers In Person at Lecture Theatre 2 Chair(s): Joxan Jaffar National University of Singapore 15:3030mTalk A Counterexample-Guided Debugger for Non-Recursive DatalogCOVID Time Papers In PersonVan-Dang Tran National Institute of Informatics, Japan, Hiroyuki Kato National Institute of Informatics, Japan, Zhenjiang Hu Peking University Link to publication DOI 16:0030mTalk A New Refinement Type System for Automated nu-HFLZ Validity CheckingCOVID Time Papers In PersonHiroyuki Katsura , Naoki Iwayama University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Takeshi Tsukada Chiba University Link to publication DOI 16:3030mTalk P3: A Profiler Suite for Parallel Applications on the Java Virtual MachineCOVID Time Papers In PersonAndrea Rosà USI Lugano, Walter Binder USI Lugano Link to publication DOI 17:0030mTalk Termination Analysis for the pi-Calculus by Reduction to Sequential Program TerminationCOVID Time Papers In PersonTsubasa Shoshi , Takuma Ishikawa The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori University of Bologna, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada Chiba University Link to publication DOI