29 citations · 78 across the 14 of their papers we have counts for
8 papers · 1 filter
Automatic HFL(Z) Validity Checking for Program Verification
Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato +1
We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reducti…
Software Model-Checking as Cyclic-Proof Search
Takeshi Tsukada, Hiroshi Unno
This paper shows that a variety of software model-checking algorithms can be seen as proof-search strategies for a non-standard proof system, known as a cyclic proof system. Our us…
Termination Analysis for the -Calculus by Reduction to Sequential Program Termination
Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi +3
We propose an automated method for proving termination of -calculus processes, based on a reduction to termination of sequential programs: we translate a -calculus process to…
Signature Restriction for Polymorphic Algebraic Effects
Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two g…
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…
Higher-Order Program Verification via HFL Model Checking
Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe
There are two kinds of higher-order extensions of model checking: HORS model checking and HFL model checking. Whilst the former has been applied to automated verification of higher…
Innocent Strategies are Sheaves over Plays---Deterministic, Non-deterministic and Probabilistic Innocence
Takeshi Tsukada, C. -H. Luke Ong
Although the HO/N games are fully abstract for PCF, the traditional notion of innocence (which underpins these games) is not satisfactory for such language features as non-determin…
A Logical Foundation for Environment Classifiers
Takeshi Tsukada, Atsushi Igarashi
Taha and Nielsen have developed a multi-stage calculus λα with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragme…