DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2026.6

Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

Authors: Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract

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 combining fractional ownership and refinement types for imperative program verification - with support for pointer arithmetic. Their idea was to extend fractional ownership so that it can depend on an array index. Their formulation, however, does not handle nested arrays, which are essential for representing practical data structures such as matrices. We extend Tanaka et al.’s type system to support nested arrays by generalizing the notion of ownership to be able to refer to the indices of the outer arrays and prove the soundness of the extended type system. We have implemented a verifier based on the proposed type system and demonstrated that it can verify the correctness of programs that manipulate nested arrays, which were beyond the reach of Tanaka et al.

Cite as

Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi. Ownership Refinement Types for Pointer Arithmetic and Nested Arrays. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 6:1-6:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fujiwara_et_al:LIPIcs.ECOOP.2026.6,
  author =	{Fujiwara, Yusuke and Matsushita, Yusuke and Suenaga, Kohei and Igarashi, Atsushi},
  title =	{{Ownership Refinement Types for Pointer Arithmetic and Nested Arrays}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{6:1--6:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.6},
  URN =		{urn:nbn:de:0030-drops-261029},
  doi =		{10.4230/LIPIcs.ECOOP.2026.6},
  annote =	{Keywords: aliasing, fractional ownership, program verification, refinement types, type systems}
}

Document

Artifact

DOI: 10.4230/DARTS.12.1.23

Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (Artifact)

Authors: Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract

This artifact accompanies the paper "Ownership Refinement Types for Pointer Arithmetic and Nested Arrays." It provides nested_array_ConSORT, a tool for automated ownership type inference and refinement type checking for imperative programs with pointer arithmetic and nested arrays. The artifact includes the tool implementation, benchmark programs, evaluation scripts to reproduce the experimental results (Tables 1, 3, 4, and 5) from the paper, and a comparison baseline (Extended_ConSORT by Tanaka et al. [Tanaka et al., 2024]). The artifact is packaged as a Docker image with all dependencies pre-installed, supporting both x86_64 and ARM64 platforms.

Cite as

Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi. Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 23:1-23:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{fujiwara_et_al:DARTS.12.1.23,
  author =	{Fujiwara, Yusuke and Matsushita, Yusuke and Suenaga, Kohei and Igarashi, Atsushi},
  title =	{{Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (Artifact)}},
  pages =	{23:1--23:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Fujiwara, Yusuke and Matsushita, Yusuke and Suenaga, Kohei and Igarashi, Atsushi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.23},
  URN =		{urn:nbn:de:0030-drops-261603},
  doi =		{10.4230/DARTS.12.1.23},
  annote =	{Keywords: aliasing, fractional ownership, program verification, refinement types, type systems}
}

Search Results

Documents authored by Fujiwara, Yusuke

Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

Abstract

Cite as

Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message