53 citations · 154 across the 20 of their papers we have counts for
5 papers · 1 filter
A Probabilistic Higher-order Fixpoint Logic
Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL an…
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…
Grammar compression with probabilistic context-free grammar
Hiroaki Naganuma, Diptarama Hendrian, Ryo Yoshinaka +2
We propose a new approach for universal lossless text compression, based on grammar compression. In the literature, a target string has been compressed as a context-free gramma…
RustHorn: CHC-based Verification for Rust Programs (full version)
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
Reduction to the satisfiability problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointe…
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
John Toman, Ren Siqi, Kohei Suenaga +2
We present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires strong updates to model changing invariants during program…