1 citations · 1 across the 3 of their papers we have counts for
4 papers
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…
Ownership Refinement Types for Pointer Arithmetic and Nested Arrays
Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga +1
Tanaka et al. proposed a type system for verifying functional correctness properties of programs that use arrays and pointer arithmetic. Their system extends ConSORT--a type system…
Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
Yusuke Matsushita, Hiromi Ishii
A promising approach to unifying functional and imperative programming paradigms is to localize mutation using linear or affine types. Haskell, a purely functional language, was re…
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…