arXiv subjects

Naoki Kobayashi

Publications and source records attributed to Naoki Kobayashi.

At least 19 recordsLinked to original sources

arXiv2026

Uniaxial stress effects on magnetic and electric properties of the ground state in a centrosymmetric magnetic skyrmion host Gd$_2$PdSi$_3$

We investigate effects of uniaxial stress to magnetic orders and electrical resistivity of the centrosymmetric magnetic skyrmion compound Gd$_2$PdSi$_3$, which has a hexagonal crystal structure composed of triangular lattice layers of magnetic Gd$^{3+}$ ions. This compound is known to exhibit the triple-$q$ magnetic skyrmion lattice phase with a giant topological Hall effect in the first field induced phase [T. Kurumaji $\textit{et al}$. Science $\textbf{365}$, 914-918 (2019)]. In contrast to the established picture of the field-induced phase, the ground state of this system still remains to be studied. Although previous studies reported the existence of the incommensurate magnetic modulations described by a magnetic modulation wave vector ${\bf q}=(q,0,0)$ where $q\sim 0.14$ and its equivalents, it is still unclear whether the magnetic structure is a single-$q$ structure or a multiple-$q$ structure. In the present study, we performed magnetization, resistivity and neutron diffraction measurements with a compressive uniaxial stress applied perpendicular to the $c$ axis. The observed data revealed that the system did not exhibit anisotropic magnetic and electric properties expected from a single-$q$ magnetic order, suggesting that the magnetic ground state of this system is a multi-$q$ magnetic order.

cond-mat.str-el↗

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\"ive 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

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\"ive 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

Solvable Tuple Patterns and Their Applications to Program Verification

Despite the recent progress of automated program verification techniques, fully automated verification of programs manipulating recursive data structures remains a challenge. We introduce solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), novel formalisms for expressing and inferring invariants between list-like recursive data structures. A distinguishing feature of STPs is that they can be efficiently inferred from only a small number of positive samples; no negative samples are required. After presenting properties and inference algorithms of STPs and CSTPs, we show how to incorporate the CSTP inference into a CHC (Constrained Horn Clauses) solver supporting list-like data structures, which serves as a uniform backend for automated program verification tools. A CHC solver incorporating the (C)STP inference has won the ADT-LIN category of CHC-COMP 2025 by a significant margin.

cs.PL↗

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↗

arXiv2024

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus

The decidability of the reachability problem for finitary PCF has been used as a theoretical basis for fully automated verification tools for functional programs. The reachability problem, however, often becomes undecidable for a slight extension of finitary PCF with side effects, such as exceptions, algebraic effects, and references, which hindered the extension of the above verification tools for supporting functional programs with side effects. In this paper, we first give simple proofs of the undecidability of four extensions of finitary PCF, which would help us understand and analyze the source of undecidability. We then focus on an extension with references, and give a decidable fragment using a type system. To our knowledge, this is the first non-trivial decidable fragment that features higher-order recursive functions containing reference cells.

cs.LO↗

arXiv2024

On Higher-Order Reachability Games vs May Reachability

We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with angelic and demonic nondeterminism) and may-reachability (i.e., the reachability problem for programs with only angelic nondeterminism). We show that reachability games for order-n programs can be reduced to may-reachability for order-(n+1) programs, and vice versa. We formalize the reductions by using higher-order fixpoint logic and prove their correctness. We also discuss applications of the reductions to higher-order program verification.

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↗

arXiv2023

Gradual Tensor Shape Checking

Tensor shape mismatch is a common source of bugs in deep learning programs. We propose a new type-based approach to detect tensor shape mismatches. One of the main features of our approach is the best-effort shape inference. As the tensor shape inference problem is undecidable in general, we allow static type/shape inference to be performed only in a best-effort manner. If the static inference cannot guarantee the absence of the shape inconsistencies, dynamic checks are inserted into the program. Another main feature is gradual typing, where users can improve the precision of the inference by adding appropriate type annotations to the program. We formalize our approach and prove that it satisfies the criteria of gradual typing proposed by Siek et al. in 2015. We have implemented a prototype shape checking tool based on our approach and evaluated its effectiveness by applying it to some deep neural network programs.

cs.PL↗

arXiv2022

Automatic HFL(Z) Validity Checking for Program Verification

We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reduction from higher-order program verification to HFL(Z) validity checking, our method yields a fully automated, uniform verification method for arbitrary temporal properties of higher-order functional programs expressible in the modal mu-calculus, including termination, non-termination, fair termination, fair non-termination, and also branching-time properties. We have implemented our method and obtained promising experimental results.

cs.PL↗

arXiv2022

A Simple and Strong Baseline for End-to-End Neural RST-style Discourse Parsing

To promote and further develop RST-style discourse parsing models, we need a strong baseline that can be regarded as a reference for reporting reliable experimental results. This paper explores a strong baseline by integrating existing simple parsing strategies, top-down and bottom-up, with various transformer-based pre-trained language models. The experimental results obtained from two benchmark datasets demonstrate that the parsing performance strongly relies on the pretrained language models rather than the parsing strategies. In particular, the bottom-up parser achieves large performance gains compared to the current best parser when employing DeBERTa. We further reveal that language models with a span-masking scheme especially boost the parsing performance through our analysis within intra- and multi-sentential parsing, and nuclearity prediction.

cs.CL↗

arXiv2021

A Probabilistic Higher-order Fixpoint Logic

We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the $μ^p$-calculus. We show that PHFL is strictly more expressive than the $μ^p$-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the $μ$-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more expressive: we give a translation from Lubarsky's $μ$-arithmetic to PHFL, which implies that PHFL model checking is $Π^1_1$-hard and $Σ^1_1$-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system.

cs.LO↗

arXiv2021

Fragmentation Statistics of Food Diced and Crushed Using a Food Mixer

The fragment-size distributions of raw carrot diced or crushed using a food mixer are studied experimentally. For the 5-mm-square raw carrot, the normal distribution shows a characteristic feature of food fragmentation statistics. This simple result indicates that most random errors contribute to fragment-size fluctuation. On the other hand, for the crushed raw carrot, the cumulative fragment size distribution follows the power law where the exponent $α\simeq 1.62 > 1$. Furthermore, considering the cumulative fragment-size distribution as a function of length for comparison with geomaterials, such as fault rocks, the exponent $D \simeq 3.64$. Previous studies have shown that the power-law distribution observed in sequential fragmentation tends to have a large exponent value. As our experiment is also based on sequential fragmentation, the obtained large values of exponents $α$ and $D$ are consistent with those obtained in previous studies on sequential fragmentation. On the basis of previous studies and our observations, we discuss the effect of the preferential fragmentation of particles as large as the mixer blades. We also discuss the existence of a lower limit beyond which further fragmentation is difficult, resulting in a power-law distribution tendency for raw carrot crushed with a food mixer.

cond-mat.soft↗

arXiv2021

Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes

We address the problem of analysing the complexity of concurrent programs written in Pi-calculus. We are interested in parallel complexity, or span, understood as the execution time in a model with maximal parallelism. A type system for parallel complexity has been recently proposed by Baillot and Ghyselen but it is too imprecise for non-linear channels and cannot analyse some concurrent processes. Aiming for a more precise analysis, we design a type system which builds on the concepts of sized types and usages. The new variant of usages we define accounts for the various ways a channel is employed and relies on time annotations to track under which conditions processes can synchronize. We prove that a type derivation for a process provides an upper bound on its parallel complexity.

cs.CC↗

arXiv2021

An Overview of the HFL Model Checking Project

In this article, we give an overview of our project on higher-order program verification based on HFL (higher-order fixpoint logic) model checking. After a brief introduction to HFL, we explain how it can be applied to program verification, and summarize the current status of the project.

cs.PL↗