Document Open Access Logo

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

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

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.12.1.23.pdf
  • Filesize: 0.67 MB
  • 6 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • aliasing
  • fractional ownership
  • program verification
  • refinement types
  • type systems

Metrics

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2026 Call for Artifacts and the ACM Artifact Review and Badging Policy.

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 Get BibTex

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) https://doi.org/10.4230/DARTS.12.1.23

Author Details

Yusuke Fujiwara
  • Kyoto University, Japan
Yusuke Matsushita
  • Kyoto University, Japan
Kohei Suenaga
  • Kyoto University, Japan
Atsushi Igarashi
  • Kyoto University, Japan

Funding

This work is partially supported by JSPS KAKENHI Grant Number 20H05703, Japan.
  • Matsushita, Yusuke: His research was supported in part also by the Hakubi Project at Kyoto University and JSPS KAKENHI Grant Number JP24KJ0133.
  • Suenaga, Kohei: His research was supported in part also by JST CREST Grant Number JPMJCR2012, Japan, and JSPS KAKENHI Grant Number 25H01113, Japan.

Acknowledgements

We thank the reviewers for their constructive comments. We are also grateful to Takashi Suwa for helping us test the artifact. The second author is currently hosted by MPI-SWS as a JSPS Overseas Research Fellow.

Related Article

  • 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), LIPIcs, Vol. 372, pp. 6:1-6:31, 2026. https://doi.org/10.4230/LIPIcs.ECOOP.2026.6

References

  1. Adrien Champion, Tomoya Chiba, Naoki Kobayashi, and Ryosuke Sato. Ice-based refinement type discovery for higher-order functional programs. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I, Lecture Notes in Computer Science, pages 365-384. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89960-2_20.
  2. Leonardo De Moura and Nikolaj Bjørner. Z3: an efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08/ETAPS'08, pages 337-340, Berlin, Heidelberg, 2008. Springer-Verlag. Google Scholar
  3. Izumi Tanaka, Ken Sakayori, and Naoki Kobayashi. Ownership types for verification of programs with pointer arithmetic. In Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, PEPM 2024, pages 94-106, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3635800.3636965.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact