Higher-order functions and imperative references are language features supported by many mainstream languages. Their combination enables the ability to package references to code blocks with the captured state from their environment. Higher-order imperative programs are expressive and useful, but complicate formal specification and reasoning due to the use of yet-to-be-instantiated function parameters, especially when their invocations may mutate memory captured by or reachable from their arguments. Existing state-of-the-art works for verifying higher-order imperative behaviors are restricted in two ways: achieving strong theoretical results without automated implementations, or achieving automation with the help of strong assumptions from dedicated type systems (e.g. Rust). To enable an automated verification solution for imperative languages without the above restrictions, we introduce Higher-order Staged Separation Logic (HSSL), an extension of Hoare logic for call-by-value higher-order functions with ML-like local references. In this paper, we design a novel staged specification logic, prove its soundness, develop a new automated higher-order verifier, Heifer, for a core OCaml-like language, report on experimental results, and present various case studies investigating its capabilities.

翻译：高阶函数和命令式引用是许多主流编程语言所支持的语言特性。二者的结合使得将代码块的引用与从环境中捕获的状态打包成为可能。高阶命令式程序具有表达力强且实用的特点，但由于使用了尚未实例化的函数参数（尤其是当这些函数的调用可能修改参数所捕获或可达的内存时），使得形式化规范与推理变得复杂。现有用于验证高阶命令式行为的最新工作在两个方面受到限制：要么在缺乏自动化实现的情况下取得强有力的理论成果，要么借助专用类型系统（如Rust）的强假设实现自动化。为了在无上述限制的前提下为命令式语言提供自动化验证方案，我们引入了高阶分阶段分离逻辑（Higher-order Staged Separation Logic, HSSL），该逻辑是对带有ML风格局部引用的按值调用高阶函数的Hoare逻辑的扩展。在本文中，我们设计了一种新颖的分阶段规范逻辑，证明了其可靠性，为类OCaml核心语言开发了新型自动化高阶验证器Heifer，报告了实验成果，并通过多种案例研究对其能力进行了探究。