arXiv subjects

Ken Sakayori

Publications and source records attributed to Ken Sakayori.

12 recordsLinked to original sources

arXiv2026

CHC-based Automated Verification of WebAssembly Programs

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 subset of WebAssembly using a constrained Horn clauses (CHCs) satisfiability solver. Our main challenges are how to handle indirect function calls effectively and how to analyze huge panic handlers. A naïve approach to the former problem would be to model a function reference table as an array of functions' entry points, but it would suffer from having too many candidates for indirect calls, resulting in a large case analysis. We address the problem by utilizing type information and filtering candidates for each indirect function call. For the latter problem, a panic handler, which is a function that is called when an error occurs, can be very large and complex. We mitigate this problem by summarizing the panic handler using control-flow analysis. We confirmed the effectiveness of our approach through preliminary experiments.

cs.PL↗

arXiv2026

Prophecy-Based Automated Verification of Message-Passing Programs

We propose a fully automated method for verifying functional correctness of message-passing concurrent programs by reducing verification problems to constrained Horn clause (CHC) solving. Inspired by RustHorn's prophecy-based technique, we represent each sender channel by a list of values to be sent over the channel in the future, which enables modular encoding of sender and receiver threads in CHCs. To capture causal dependencies between different channels, we further attach timestamps to messages. We prove that the resulting reduction is sound and complete: a program is free from assertion failures if and only if the corresponding system of CHCs is satisfiable. We have also implemented a prototype verifier for Rust-like programs and experimentally confirmed the effectiveness of the approach.

cs.PL↗

arXiv2026

Wiring the Pi-calculus to Denotational Semantics

We introduce a dialect of the Asynchronous pi-calculus, called AWpi, in which (1) an input name may be owned, at any time, by at most one process; (2) each name has either only the input or only the output capability. As a result, special processes called wires (aka forwarders, that is, processes that receive values at one name and re-transmit) behave as substitutions when composed with any AWpi process. Thus AWpi naturally yields a category, whose morphisms are AWpi processes (modulo the reference behavioural equivalence, barbed congruence) and whose objects are types; and where wires act as identity morphisms. We show that the category of processes can be further organised into (sub)categories with the structures needed for the interpretation of common higher-order language features in the literature by drawing on insights from game semantics; notably, we construct a relative Seely category, the categorical structure that concurrent game semantics has. At the same time, AWpi follows the tradition of ordinary pi-calculi in that expressiveness is preserved and the operational and algebraic theory are developed in a similar manner, notwithstanding substantial technical differences in their development and proofs. In short, the goal of AWpi is to remain faithful to the operational and algebraic tradition of the pi-calculi while connecting to the tradition of denotational models for programming languages.

cs.LO↗

arXiv2026

Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers

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 bugs by reducing reference counting verification to an assertion checking problem leveraging the Linux driver interface. Through efficient modeling of the Linux kernel and aggressive program slicing, DrvHorn discovered 545 bugs, of which 424 were previously unknown, across all platform drivers in v6.6 Linux kernel, with a lower false positive rate of 29.9% compared to prior studies. To address the root causes of these newly discovered bugs, we submitted patches to the Linux kernel, and 45 of them were merged.

cs.CR↗

arXiv2026

Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators

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 off-chip bandwidth utilization. However, even with HLS, designing such systems still requires careful manual tuning, as automatic optimizations provided by existing tools are highly sensitive to programming style and often lack transparency. To address these issues, we present a formal translation framework based on relational Hoare logic, which enables robust and transparent transformations. Our method recognizes complex memory access patterns in naïve HLS programs and automatically transforms them by inserting on-chip buffers to enforce linear access to off-chip memory, and by replacing non-sequential processing with stream processing, while preserving program semantics. Experiments using our prototype translator, combined with an off-the-shelf HLS compiler and a real FPGA board, have demonstrated significant performance improvements.

cs.PL↗

arXiv2025

On Circuit Description Languages, Indexed Monads, and Resource Analysis

In this paper, a monad-based denotational model is introduced and shown adequate for the Proto-Quipper family of calculi, themselves being idealized versions of the Quipper programming language. The use of a monadic approach allows us to separate the value to which a term reduces from the circuit that the term itself produces as a side effect. In turn, this enables the denotational interpretation and validation of rich type systems in which the size of the produced circuit can be controlled. Notably, the proposed semantic framework, through the novel concept of circuit algebra, suggests forms of effect typing guaranteeing quantitative properties about the resulting circuit, even in presence of optimizations.

cs.PL↗

arXiv2025

Extensional and Non-extensional Functions as Processes

Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure $λ$-calculus, the process representations yield (at best) non-extensional $λ$-theories (i.e., $β$ rule holds, whereas $η$ does not). In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal $π$, $\mathrm{I}π$ (a subset of the $π$-calculus in which all outputs are bound), we develop a refinement of Milner's original encoding of functions as processes that is parametric on certain abstract components called wires. These are, intuitively, processes whose task is to connect two end-point channels. We show that when a few algebraic properties of wires hold, the encoding yields a $λ$-theory. Exploiting the symmetries and dualities of $\mathrm{I}π$, we isolate three main classes of wires. The first two have a sequential behaviour and are dual of each other; the third has a parallel behaviour and is the dual of itself. We show the adoption of the parallel wires yields an extensional $λ$-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite $η$. In contrast, the other two classes of wires yield non-extensional $λ$-theories whose equalities are those of the Lévy-Longo and Böhm trees.

cs.LO↗

arXiv2025

Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types

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 attention in recent years, leading to the development of various CHC solvers. However, existing solvers for CHCs over ADTs are not fully satisfactory, due to their limited ability to find and express models involving inductively defined functions/predicates (e.g., those about the sum of list elements). To address this limitation, we consider catamorphisms (generalized fold functions), and present a framework for automatically discovering appropriate catamorphisms on demand and using them to express a model of given CHCs. We have implemented a new CHC solver called Catalia based on the proposed method. Our experimental results for the CHC-COMP 2024 benchmark show that Catalia outperforms state-of-the-art solvers in solving satisfiable CHCs over ADTs. Catalia was also used as a core part of the tool called ChocoCatalia, which won the ADT-LIA category of CHC-COMP 2025.

cs.LO↗

arXiv2023

Ownership Types for Verification of Programs with Pointer Arithmetic

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 refinement types in the presence of pointer aliases. We extend their type system to support pointer arithmetic, and prove its soundness. Based on the proposed type system, we have implemented a prototype tool for automated verification of the lack of assertion errors of low-level programs with pointer arithmetic, and confirmed its effectiveness through experiments.

cs.PL↗

arXiv2023

Borrowable Fractional Ownership Types for Verification

Automated verification of functional correctness of imperative programs with references (a.k.a. pointers) is challenging because of reference aliasing. Ownership types have recently been applied to address this issue, but the existing approaches were limited in that they are effective only for a class of programs whose reference usage follows a certain style. To relax the limitation, we combine the approaches of ConSORT (based on fractional ownership) and RustHorn (based on borrowable ownership), two recent approaches to automated program verification based on ownership types, and propose the notion of borrowable fractional ownership types. We formalize a new type system based on the borrowable fractional ownership types and show how we can use it to automatically reduce the program verification problem for imperative programs with references to that for functional programs without references. We also show the soundness of our type system and the translation, and conduct experiments to confirm the effectiveness of our approach.

cs.PL↗

arXiv2021

Termination Analysis for the $π$-Calculus by Reduction to Sequential Program Termination

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 a sequential program, so that the termination of the latter implies that of the former. We can then use an off-the-shelf termination verification tool to check termination of the sequential program. Our approach has been partially inspired by Deng and Sangiorgi's termination analysis for the $π$-calculus, and checks that there is no infinite chain of communications on replicated input channels, by converting such a chain of communications to a chain of recursive function calls in the target sequential program. We have implemented an automated tool based on the proposed method and confirmed its effectiveness.

cs.PL↗

arXiv2021

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving

Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of symbolic automatic relations (SARs), which combines symbolic automata and automatic relations, and inherits their good properties such as the closure under Boolean operations. We consider the satisfiability problem for SARs, and show that it is undecidable in general, but that we can construct a sound (but incomplete) and automated satisfiability checker by a reduction to CHC solving. We discuss applications to SMT and CHC solving on data structures, and show the effectiveness of our approach through experiments.

cs.LO↗