2 papers
cs.PL2026
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…
cs.PL2023
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…