1 citations · 2 across the 7 of their papers we have counts for
8 papers
CHC-based Automated Verification of WebAssembly Programs
Akihisa Yagi, Ken Sakayori, Naoki Kobayashi
WebAssembly is a stack-based imperative language widely used to develop safe and efficient Web applications. In this paper, we propose an automated static verification method for a…
Prophecy-Based Automated Verification of Message-Passing Programs
Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi +2
We propose a fully automated method for verifying functional correctness of message-passing concurrent programs by reducing verification problems to constrained Horn clause (CHC) s…
Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers
Joe Hattori, Naoki Kobayashi, Ken Sakayori
Reference counting bugs in Linux kernel drivers can lead to severe resource mismanagement and security vulnerabilities. We introduce DrvHorn, a novel automated tool to detect these…
Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators
Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki +1
High-level synthesis (HLS) is a powerful tool for developing efficient hardware accelerators that rely on specialized memory systems to achieve sufficient on-chip data reuse and of…
Solvable Tuple Patterns and Their Applications to Program Verification
Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara +1
Despite the recent progress of automated program verification techniques, fully automated verification of programs manipulating recursive data structures remains a challenge. We in…
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori +1
We propose a novel approach to satisfiability checking of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). CHC-based automated verification has gained considerable…
Ownership Types for Verification of Programs with Pointer Arithmetic
Izumi Tanaka, Ken Sakayori, Naoki Kobayashi
Toman et al. have proposed a type system for automatic verification of low-level programs, which combines ownership types and refinement types to enable strong updates of refinemen…
Borrowable Fractional Ownership Types for Verification
Takashi Nakayama, Yusuke Matsushita, Ken Sakayori +2
Automated verification of functional correctness of imperative programs with references (a.k.a. pointers) is challenging because of reference aliasing. Ownership types have recentl…