1 citations · 4 across the 5 of their papers we have counts for
4 papers · 1 filter
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
Takumi Shimoda, Naoki Kobayashi, Ken Sakayori +1
Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT…
A Cyclic Proof System for HFLN
Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi
A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFLN, which is a higher-order predicate logic with…
A Type-Based HFL Model Checking Algorithm
Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown th…
Proceedings Eighth Workshop on Intersection Types and Related Systems
Naoki Kobayashi
This volume contains a final and revised selection of papers presented at the Eighth Workshop on Intersection Types and Related Systems (ITRS 2016), held on June 26, 2016 in Porto,…