1 citations · 2 across the 7 of their papers we have counts for
4 papers · 1 filter
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…