一句话：通过引入不稳定资源并调整帧规则，使 Iris 支持堆依赖表达式断言并连接 SMT 求解器。
Iris 分离逻辑框架假定所有断言都稳定，因而可无条件使用帧规则；这带来模块化推理，却排除了 Viper 验证器家族的核心特性——堆依赖表达式断言，后者能把程序表达式提升到断言层，减少代码与规约冗余并利于 SMT 自动化。本文提出 Daenerys：先重新审视 Iris 核心，引入新的不稳定资源并调整帧规则；再构建支持堆依赖表达式断言的程序逻辑，并奠定连接 Iris 与 SMT 求解器的基础。作者用多个案例研究评估，部分案例超出 Viper 和 Iris 各自能力，另一些受益于 SMT 连接。
The separation logic framework Iris has been built on the premise that all assertions are stable , meaning they unconditionally enjoy the famous frame rule. This gives Iris—and the numerous program logics that build on it—very modular reasoning principles. But stability also comes at a cost. It excludes a core feature of the Viper verifier family, heap-dependent expression assertions , which lift program expressions to the assertion level in order to reduce redundancy between code and specifications and better facilitate SMT-based automation. In this paper, we bring heap-dependent expression assertions to Iris with Daenerys . To do so, we must first revisit the very core of Iris, extending it with a new form of unstable resources (and adapting the frame rule accordingly). On top, we then build a program logic with heap-dependent expression assertions and lay the foundations for connecting Iris to SMT solvers. We apply Daenerys to several case studies, including some that go beyond what Viper and Iris can do individually and others that benefit from the connection to SMT.
@article{paperbot3102,
title = {Destabilizing Iris},
author = {Simon Spies and Niklas Mück and Haoyi Zeng and Michael Sammler and Andrea Lattuada and Peter Müller and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729284}
}