Combining higher-order model checking with refinement type inference. - Ryosuke Sato 001; Naoki Iwayama; Naoki Kobayashi 001 (PEPM@POPL, 2019)

A New Refinement Type System for Automated $ nu text {HFL}_ mathbb {Z}$ Validity Checking. - Hiroyuki Katsura; Naoki Iwayama; Naoki Kobayashi 001; Takeshi Tsukada (APLAS, 2020)

Predicate Abstraction and CEGAR for $ nu mathrm {HFL}_ mathbb {Z}$ Validity Checking. - Naoki Iwayama; Naoki Kobayashi 001; Ryota Suzuki 002; Takeshi Tsukada (SAS, 2020)