paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Sound up-to techniques and Complete abstract domains

健全的 up-to 技术与完备抽象域
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 3/10 · 论文属于抽象解释与余归纳的理论工作，与程序分析和形式化验证基础相关，但未涉及用户关注的 LLM/Agent 交叉、浮点程序分析或贝叶斯程序分析等核心方向，因此匹配度较低。引用 0 inbox
Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, Dusko Pavlovic
程序分析与抽象解释形式语义
crossref: 2026-09-12

AI 速览

一句话：研究 sound up-to 技术与完备抽象域之间的关系，连接余归纳与抽象解释。

本文关注抽象解释与余归纳之间的关系。抽象解释是一种自动寻找程序或代码片段不变量的方法，其语义由最小不动点给出；而 up-to 技术则被提出用于增强余归纳，后者是证明由最大不动点表达的性质的抽象原则。论文以 sound up-to techniques 和 complete abstract domains 为核心，试图在分别面向最小不动点与最大不动点的两类推理方法之间建立联系。摘要仅给出研究背景与基本定位，未提供具体技术构造、定理结果或实验评估。

问题
如何将用于最大不动点性质证明的余归纳 up-to 技术与用于最小不动点语义的抽象解释联系起来，并刻画其健全性与完备抽象域。
方法
摘要未披露具体方法，仅表明论文围绕 sound up-to 技术与 complete abstract domains 展开理论分析。
评估
摘要未报告评估方式；从内容看属于理论性研究，未提供实验或案例验证信息。
原文摘要（Abstract）

Abstract interpretation is a method to automatically find invariants of programs or pieces of code whose semantics is given via least fixed-points. Up-to techniques have been introduced as enhancements of coinduction, an abstract principle to prove properties expressed via greatest fixed-points.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot4355,
  title = {Sound up-to techniques and Complete abstract domains},
  author = {Filippo Bonchi and Pierre Ganty and Roberto Giacobazzi and Dusko Pavlovic},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209169}
}