Verification for Program Manipulations using Iris

DOI

10.2991/978-94-6239-638-8_2How to use a DOI?

Keywords

program verification; metaprogramming; program logic; Iris

Abstract

In this paper, we implement a framework for verifying programs targeting source code using the theorem prover Rocq and the program logic library Iris. As programming languages become more complex, it is becoming difficult to accurately describe their semantics. As a result, it is becoming increasingly difficult to predict the semantic issues that will arise when language extensions are added. In systems that perform static source code changes, such as macro and template metaprogramming, users can change syntax without affecting semantics. The proposed framework performs data-source mapping in the verification system, similar to metaprogramming, to extract another program from the data during program execution and verify its semantics. This paper verifies that the proposed method enables program verification of this kind.

Copyright

© 2026 The Author(s)

Open Access

Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Download article (PDF)

TY  - CONF
AU  - Sosuke Moriguchi
PY  - 2026
DA  - 2026/04/30
TI  - Verification for Program Manipulations using Iris
BT  - Proceedings of the  Workshop on Computation: Theory and Practice (WCTP 2025)
PB  - Atlantis Press
SP  - 7
EP  - 16
SN  - 2589-4900
UR  - https://doi.org/10.2991/978-94-6239-638-8_2
DO  - 10.2991/978-94-6239-638-8_2
ID  - Moriguchi2026
ER  -