Foundational verification considers the functional correctness of programming languages with formalized semantics and uses proof assistants (e.g., Coq, Isabelle) to certify proofs. The need for verifying complex programs compels it to involve expressive Separation Logics (SLs) that exceed the scopes of well-studied automated proof theories, e.g., symbolic heap. Consequently, automation of SL in foundational verification relies heavily on ad-hoc heuristics that lack a systematic meta-theory and face scalability issues. To mitigate the gap, we propose a theory to specify SL predicates using abstract algebras including functors, homomorphisms, and modules over rings. Based on this theory, we develop a generic SL automation algorithm to reason about any data structures that can be characterized by these algebras. In addition, we also present algorithms for automatically instantiating the algebraic models to real data structures. The instantiation reuses the algebraic models of component structures and preserves their data abstractions. Case studies on formalized imperative semantics show our algorithm can instantiate the algebraic models automatically for a variety of complex data structures. Experimental results indicate the automatically instantiated reasoners from our generic theory show similar results to the state-of-the-art systems made of specifically crafted reasoning rules. The presented theories, proofs, and the verification framework are formalized in Isabelle/HOL.

翻译：基础验证关注具有形式化语义的编程语言的功能正确性，并使用证明辅助工具（如Coq、Isabelle）来认证证明。验证复杂程序的需求迫使其涉及超出已有成熟自动化证明理论（如符号堆）范围的表达性分离逻辑。因此，基础验证中分离逻辑的自动化严重依赖缺乏系统元理论且面临可扩展性问题的临时启发式方法。为弥补这一差距，我们提出一种理论，使用包括环上的函子、同态和模在内的抽象代数来规范分离逻辑谓词。基于该理论，我们开发了一种泛化分离逻辑自动化算法，可用于推理任何能被这些代数刻画的数据结构。此外，我们还提出了将代数模型自动实例化为实际数据结构的算法。该实例化过程复用组件结构的代数模型，并保持其数据抽象。对形式化命令式语义的案例研究表明，我们的算法能够为多种复杂数据结构自动实例化代数模型。实验结果表明，从我们泛化理论自动实例化的推理器与由专门设计的推理规则构成的最先进系统具有相近的效果。所提出的理论、证明及验证框架均在Isabelle/HOL中形式化实现。