Correctness Kernels of Abstract Interpretations
在基于抽象解释的静态分析中，近似是由抽象域编码的。它们为设计抽象语义函数提供了系统的指导，这些抽象语义函数近似于分析中的某些具体系统行为。为了近似给定的具体语义功能，抽象域可能包含冗余信息。本文介绍了抽象解释的正确性核的概念，一种简化抽象域的方法，即从它们中删除抽象值，以最大的方式，同时保留完全相同的近似行为的系统分析。我们表明，在抽象的模型检验正确性内核提供了一个由示例指导的抽象状态空间的简化范例，这意味着这种简化保留了示例的虚假性（即，抽象路径）。特别是，我们展示了如何正确的内核可以集成与著名的CEGAR（反例引导的抽象细化）方法。
2013-04-19 cs.LO cs.PL
A proof-theoretic approach to abstract interpretation
Google Inc.（谷歌公司）；Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；University of Johannesburg（约翰内斯堡大学）；University of Luxembourg（卢森堡大学）；INRIA（法国国家信息与自动化研究所）
本文通过将逻辑系统与有限抽象系统关联，提出了一种生成与抽象格同构的Lindenbaum-Tarski代数的逻辑的通用程序，并建立了相应的可靠性和完备性结果。
2026-05-26 cs.LO math.LO
On the Monniaux Problem in Abstract Interpretation
抽象解释中的Monniaux问题，粗略地说，询问以下问题是否是可判定的：给定程序$P$，安全（\emph{e.g.}，不可达性）规范$φ$，和不变量$\mathcal{D}$的抽象域，在$\mathcal{D}$中是否存在归纳不变$I$，保证程序$P$满足其规范$φ$。当然，Monniaux问题是由程序的类别和人们所考虑的不变域参数化的。在本文中，我们证明了Monniaux问题是不可判定的无保护仿射规划和半线性不变量（联盟多面体）。此外，我们发现，可判定性恢复的重要特殊情况下，简单的线性循环。
2019-07-18 cs.LO
Injecting Abstract Interpretations into Linear Cost Models
我们提出了一个基于语义的框架，用于分析程序的资源使用的定量行为。我们从一个带有成本的操作语义开始。成本集的双曲面结构允许将定量语义定义为线性算子。然后，我们提出了一个抽象的抽象技术的启发，从抽象的解释，以有效地计算全局成本信息的程序。抽象必须考虑两个不同的顺序概念：成本顺序和状态顺序。我们表明，我们的抽象技术提供了一个正确的近似的具体成本计算。
2010-06-26 cs.LO cs.PL
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
研究正确性与错误性变换程序逻辑，扩展以处理终止与非终止，证明其为自然关系语义的抽象解释，提供计算化方法设计可靠完备证明系统，并扩展 Hoare 逻辑及设计新前置条件逻辑。
2023-11-23 cs.LO
An Approach to the Abstract Interpretation of Goal-Directed Answer Set Programming
IMDEA Software Institute（IMDEA软件研究所）；University of Texas at Dallas（德克萨斯大学达拉斯分校）；Spanish Council for Scientific Research (CSIC)（西班牙国家科学研究委员会）
该研究针对目标导向答案集编程，提出基于PLAI不动点的自顶向下算法及共享约束抽象域，通过三个应用研究其在s(CASP)中的实用性，证明编译时静态分析可改进目标导向ASP程序评估。
2026-07-23 cs.LO
Abstract Program Slicing: an Abstract Interpretation-based approach to Program Slicing
在本文中，我们正式定义了抽象程序切片的概念，程序切片的一般形式被认为是数据的属性，而不是它们的确切值。这种方法适用于具有数值和引用值的语言，并依赖于程序组件（语句）之间的抽象依赖关系的概念。不同形式的（后向）抽象切片被添加到现有的正式框架中，传统的非抽象形式的切片可以进行比较。扩展的框架使我们能够理解抽象切片是传统切片的推广，因为传统切片（处理语法依赖关系）是由（语义）非抽象形式的切片推广的，这实际上相当于对数据执行身份抽象的抽象形式。声音算法计算抽象的依赖关系和程序片的系统表征，它依赖于程序状态之间的协议的概念。
2016-05-17 cs.LO cs.PL
Sequence-Based Abstract Interpretation of Prolog
针对现有Prolog抽象解释框架无法覆盖部分控制结构的问题，提出基于替换序列、可处理深度优先搜索与cut操作符的新框架，证明其适配传统抽象域且可涵盖此前的确定性分析工作，实验验证了有效性。
2000-10-19 cs.LO cs.PL
Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
抽象解释、霍尔逻辑和不正确（或反向霍尔）逻辑是静态分析计算机程序的强大技术。所有这些都已成功地扩展到量子设置，但在很大程度上是并行开发的。在本文中，我们研究这些技术之间的关系，在验证量子while程序的背景下，其中的抽象域和一组断言的量子状态是结构良好的。特别地，我们证明了任何完全的量子抽象解释都可以导出一个量子霍尔逻辑和一个量子不正确逻辑，这两个逻辑都是合理的和相对完备的。与文献中提出的逻辑不同，诱导逻辑系统是以向前的方式，使它们在某些应用中更有用。相反，任何健全的和相对完整的量子霍尔逻辑或量子不正确逻辑都导出一个完整的量子抽象解释。作为应用，我们证明了当局部子空间元组作为断言时，不存在任何可靠的、相对完备的量子霍尔逻辑或不正确逻辑.
2022-06-28 cs.LO quant-ph
Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation
Paige和Tarjan算法（PT）用于计算状态划分的粗细化，这是一些Kripke结构上的互模拟是众所周知的。在模型检验中，互模拟等价于CTL的强保持，或者等价于Hennessy-Milner逻辑的强保持。根据这些观察，我们分析了PT算法的基本步骤，从抽象解释的角度来看，这使我们能够在通用归纳定义（时态）语言和抽象解释指定的可能非分区抽象模型的背景下进行强保护。这使我们设计了一个广义的Paige-Tarjan算法，称为GPT，用于计算一个抽象的基于解释的模型，强烈保留一些给定的语言的最小细化。证明了在强保持Hennessy-Milner逻辑的情况下，PT是GPT在状态划分域上的直接实例。我们提供了一些例子，说明GPT是通用的。我们首先展示了如何一个众所周知的有效算法计算口吃等价可以被视为一个简单的实例GPT。然后，我们实例化GPT，以设计一个新的高效的算法计算仿真等价，是最好的算法竞争。最后，我们展示了GPT如何允许计算新的强保持抽象模型，通过提供一个有效的算法，计算一个给定的分区，强烈保留的语言生成的可达性运算符的coarthorough细化。
2006-12-27 cs.LO
Abstract Interpretation for Probabilistic Termination of Biological Systems
在以前的论文中，作者应用抽象解释方法近似生物系统的概率语义，专门使用化学基型演算建模。该方法是基于代表一组实验的想法，这只是不同的初始浓度，通过抽象的多重性的试剂存在于溶液中，使用间隔。在本文中，我们改进的方法，以解决概率终止属性。更详细地说，我们引入了一个细化的抽象LTS语义，我们抽象的概率语义使用的区间马尔可夫链的变体。抽象的概率模型安全地近似一组具体的实验和报告保守的下限和上限的概率终止。
2009-11-26 cs.CE cs.FL cs.LO
Abstract Interpretation with Unfoldings
我们提出并评估了一种技术，用于计算路径敏感的并发程序的抽象解释过程中的干扰条件。代替不动点计算，我们使用素事件结构来compensate表示因果关系的依赖性和干扰之间的序列的变压器。我们的主要贡献是一个展开算法，使用一个新的概念的独立性，以避免冗余的Transformer应用程序，线程本地固定点，以减少展开的大小，和一个新的截断标准的基础上包容，以保证终止的分析。我们的实验表明，抽象展开产生一个数量级的假警报比一个成熟的抽象解释器，而几个数量级的速度比求解器为基础的工具，具有相同的精度。
2017-05-01 cs.LO cs.PL
Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday
这本书是一本散文集，从个人回忆到技术贡献。这是对戴夫·施密特和他的职业生涯的致敬，并在他六十岁生日之际创作。
2013-09-18 cs.LO cs.PL cs.SE
Combining Forward and Backward Abstract Interpretation of Horn Clauses
前向分析和后向分析的交替是程序抽象解释中的一种标准技术，当我们希望证明某些不需要的程序状态不可达时，这种技术特别有用。当前用于组合Horn子句的前向（在逻辑编程术语中为自底向上）和后向（自顶向下）抽象解释的最先进技术是查询-应答转换。它转换了Horn子句系统，使得标准的前向分析可以从目标向前和向后传播约束。问答转换是有效的，但有我们希望解决的问题。为此，我们引入了一个新的后向收集语义，它适用于交替的前向和后向抽象解释的Horn子句。我们展示了如何交替可以用来证明无法达到的目标，以及如何每一个后续运行的分析产生一个完善的系统模型。实验上，我们观察到，结合向前和向后的分析是很重要的分析系统编码的问题，在C程序的可达性。特别是，遵循我们的新语义的组合提高了我们自己的抽象解释器的精度，包括与查询-答案转换系统的前向分析相比。
2017-08-07 cs.LO cs.PL
Quantum Set Theory Extending the Standard Probabilistic Interpretation of Quantum Theory (Extended Abstract)
两个观测量相等的概念在量子理论的基础中起着重要的作用。然而，基于传统玻恩公式的标准概率解释并没有给出一对任意观测量的概率相等关系，因为玻恩公式只给出了可交换观测量族的概率分布。本文利用Takeuti和本文作者发展的量子集合论，系统地推广了量子理论的概率解释，定义了一对任意可观测量的相等关系的概率。这种新的解释测量理论的应用进行了简要讨论。
2014-12-30 cs.LO quant-ph
An Experiment Combining Specialization with Abstract Interpretation
以前的研究表明，控制流细化可以通过一个程序专门化结合基于属性的抽象来实现，以提高终止和复杂性分析工具。我们现在表明，这个专门构建的专门化程序可以以更模块化的方式进行重构，并且可以使用现成的部分评估工具来实现先前的结果，并将其应用于抽象解释器。抽象解释器的关键特征是抽象域，它是基于属性的抽象域与具体域的乘积。这种独立于语言的框架提供了一种实用的方法来实现各种强大的专门化，并有助于使用解释器和专门化来实现程序转换的研究。
2020-08-07 cs.LO cs.PL cs.SC
Abstract Interpretation in Formal Argumentation: with a Galois Connection for Abstract Dialectical Frameworks and May-Must Argumentation (First Report)
Nagoya Institute of Technology（名古屋工业大学）
基于标签的形式论证依赖于标签函数，通常分配3个标签之一来指示每个参数的接受，拒绝或未决定。虽然经典的基于标记的方法应用全局统一的条件来标记参数，但它们可以在每个参数上更局部地确定。抽象辩证框架（ADF）是一个著名的论证形式主义，属于这一类，提供了更大的标签灵活性。然而，随着论证的规模在论证和论证对论证关系的数量上的增加，检查标记函数是否满足这些局部条件或者甚至检查这些条件是否符合指定它们的人的意图变得越来越昂贵。因此，在对一个更大的论证进行推理时，需要某种妥协。在这方面，有一个最近提出的形式主义的可能必须论证（MMA），强制执行仍然是本地的，但更抽象的标签条件。我们确定他们如何在这项工作中相互联系。我们证明了它们之间存在伽罗瓦连接，其中ADF是MMA的具体化，MMA是ADF的抽象。我们探讨了抽象解释在正式论证中发挥作用的后果，展示了一个合理的推理，从MMA内ADF的可接受性/可拒绝性的判断。据我们所知，很少有任何工作，将抽象的解释纳入正式的论证在文献中，并在规定的情况下，这项工作是第一个证明其使用和相关性。
2020-07-22 cs.AI cs.LO
Quantum entanglement analysis based on abstract interpretation
纠缠是量子态的一种非定域性质，在量子信息论中起着决定性的作用。一些协议，如隐形传态，是基于量子纠缠态。此外，任何不产生纠缠的量子算法都可以在经典计算机上有效地模拟。然而，纠缠的确切作用还没有得到很好的理解。由于纠缠演化的精确分析会导致指数减速，我们考虑基于抽象解释框架的近似分析。本文将一种基于超算子的具体量子语义与一种简单的量子程序设计语言联系起来。纠缠的表示，即抽象域的设计是一个关键问题。选择纠缠作为存储器的分区的表示。一个抽象的语义介绍，并证明了近似的可靠性。
2008-01-28 cs.LO cs.PL quant-ph
Abstract Interpretation of Temporal Concurrent Constraint Programs
时间并发约束编程（Timed Concurrent Constraint Programming，tcc）是一种声明式的并发模型，提供了一种用于指定反应式系统（reactive systems）的逻辑，即与环境持续交互的系统。通用tcc形式主义（utcc）是tcc的扩展，具有表示移动性的能力。这里，移动性被理解为私有名称的通信，如通常针对移动系统和安全协议所做的。在本文中，我们考虑了tcc的指称语义，并将其扩展为基于约束序列上的闭包运算符的utcc的“收集”语义。依靠这种语义，我们形式化了一个通用框架的数据流分析的tcc和utcc程序的抽象解释技术。我们提出的具体和抽象语义是组合的，从而使我们能够减少数据流分析的复杂性。我们表明，我们的方法是健全的和参数的抽象域。因此，可以通过实例化框架来执行不同的分析。我们说明了如何可以重用抽象域先前定义的逻辑编程执行，例如，接地分析TCC程序。我们展示了这种分析在反应系统的背景下的适用性。此外，我们还利用抽象语义来展示一个安全协议中的秘密缺陷。我们还展示了如何有可能作出分析，这可能表明，tcc程序暂停免费。这对于多种用途都很有用，例如优化编译或调试。
2013-12-09 cs.LO
Calculational Design of Hyperlogics by Abstract Interpretation
本文通过抽象解释原理设计了用于证明迭代程序超性质的通用不动点抽象解释器，推导出下近似与上近似超逻辑，并提出多种代数抽象以简化证明规则，实现了超逻辑的新代数泛化。
2024-11-17 cs.LO
Sound up-to techniques and Complete abstract domains
抽象解释是一种自动寻找程序或代码不变量的方法，其语义通过最少不动点给出。上至技术已经被引入作为共归纳的增强，共归纳是一个抽象的原则，用来证明通过最大不动点表示的属性。虽然抽象解释从定义上讲总是合理的，但最新技术的合理性需要一些独创性来证明。为了完整性，设置进行了切换：最新技术总是完整的，而抽象领域则不然。在这项工作中，我们表明，在合理的假设下，有一个明显的连接之间的声音高达技术和完整的抽象域。
2018-05-02 cs.LO
Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version)
我们提出了一种技术，用于从自然语义规范的程序设计语言的语义程序分析。该技术基于一种特殊的语义，称为pretty-big-step语义。我们提出了一个漂亮的大步骤语义的语言与简单的对象称为O 'While，并指定了一系列的仪表的语义，明确了流程的值在程序中。这导致了基于语义的依赖性分析，在核心，例如，污染分析在软件安全中的应用用Coq证明助手实现了形式化。
2013-09-20 cs.LO cs.PL
Parf: Adaptive Parameter Refining for Abstract Interpretation
针对抽象解释静态分析器参数依赖专家调优的问题，本文提出全自动框架 Parf，通过格状空间上的概率分布增量精化参数，并在 Frama-C/Eva 与 OSCS 基准上显著降低误报。
2024-09-09 cs.LO
Elusive but Coverable: The Recursion-Theoretic Structure of Complete Abstract Interpretations
University of Arizona（亚利桑那大学）
从递归理论角度研究抽象解释的局部完备性与不完备性，刻画静态和动态程序分析区别，证明诱导局部完备谓词变换器的程序类难以捉摸但有可判定覆盖，可通过程序转换构造有效枚举。
2026-07-13 cs.LO cs.PL
An efficient simulation algorithm based on abstract interpretation
计算模拟前序的算法有很多。Sigma表示状态空间，->表示转移关系，Psim表示由模拟等价引起的Sigma的划分。Henzinger、Henzinger、Kopke和Bloom和Paige的算法都是O（|Sigma||->|）-时间，并且就时间复杂度而言，它们是最好的可用算法。然而，这些算法具有空间复杂度的缺点，该空间复杂度在状态空间的大小上大于二次方。Gentilini，Piazza，Policriti的算法--后来由van Glabbeek和Ploeger修正--似乎提供了时间和空间复杂度之间的最佳折衷。Gentilini等人的算法运行时间为O（|Psim| ^2|->|）-time，而空间复杂度为O（|Psim| ^2 + |Sigma| log |Psim|）。我们在这里提出了一个新的高效的仿真算法，获得作为修改Henzinger等人。的算法，其正确性基于抽象解释在模型检验中的应用中所使用的一些技术。算法的时间复杂度为O（|Psim||->|）-时间和O（|Psim| |Sigma| log |Sigma|）-空间。因此，该算法改进了已知的最佳时间界限，同时保持了可接受的空间复杂度，该空间复杂度通常小于状态空间大小的二次方。实验评价表明，良好的比较结果与Henzinger，Henzinger和Kopke的算法。
2008-12-05 cs.LO
Context-Sensitive Abstract Interpretation of Dynamic Languages
针对动态语言IDE工具因动态特性导致控制流/数据流识别失效的问题，提出基于抽象解释的静态分析算法，可分析动态元编程与反射，已实现支持JavaScript子集的原型分析器，弥合动静态语言工具差距。
2024-01-31 cs.LO cs.PL cs.SE
Multivariant Assertion-based Guidance in Abstract Interpretation
在程序分析中，近似是一种必要的恶，因为它们确保了基本的属性，例如分析的可靠性和终止性，但它们也意味着不总是产生有用的结果。已经研究了自动技术以防止精度损失，通常以较大的资源消耗为代价。在这两种情况下（即，当分析产生不准确的结果时，以及当资源消耗太高时），有必要为用户提供某种手段来提供信息以指导分析，从而提高精度和/或性能。我们提出了一个抽象的解释框架内支持一组丰富的断言，可以处理多变量/上下文敏感性，并可以处理不同的运行时语义的断言，不能在编译时放电的技术。我们将展示如何将所提出的方法应用于提高精度和加速分析。我们还提供了一些正式的结果，这样的断言上的分析结果的影响。
2018-12-17 cs.LO cs.PL
Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
我们提出了一种方法来约束霍恩子句（CHC）验证相结合的三种技术：抽象的解释在一个域的凸多面体，专门化的约束条件在CHC使用抽象解释的查询答案转换的条款，和细化分裂谓词。的工作的目的是调查如何分析和转换工具开发的约束逻辑程序（CLP）可以适用于霍恩子句验证问题。凸多面体的抽象解释能够推导出复杂的不变量，当与传播约束的专业化结合使用时，它可以经常解决具有挑战性的验证问题。这本身就是一个贡献，但是当它失败时需要精化，并且如何精化凸多面体分析的问题还没有被研究很多。我们提出了一种改进技术的基础上插值来自一个反例跟踪，这些都是用来驱动基于属性的专业化，分裂谓词，进而导致更精确的凸多面体分析。专业化，分析和分裂的过程可以重复，以类似于CEGAR和迭代专业化方法的方式。
2014-12-03 cs.LO
Source-to-source optimizing transformations of Prolog programs based on abstract interpretation
在不改变其操作语义的情况下，通过转换源代码使Prolog程序更有效，这不是一个显而易见的任务。它要求用户清楚地了解Prolog编译器是如何工作的，特别是不纯的特性（如cut）的影响。编写Prolog代码的方式-例如，从句的顺序、从句中字面意思的顺序、删减或否定的使用--都会影响其效率。此外，不同的优化技术在一起应用时可能是冗余的或冲突的，这取决于调用过程的方式-例如，插入切口并启用索引。我们提出了一个优化器，基于抽象的解释，自动执行安全的代码转换的Prolog程序的上下文中的一些类的输入调用。如果过程用关于模式、类型、共享、解决方案的数量等的附加信息来注释，则该方法更有效。因此，该方法与Mercury类似。它适用于任何Prolog程序。
2007-10-31 cs.LO cs.PL cs.SE
A fully-abstract semantics of lambda-mu in the pi-calculus
我们研究了Muda-mu演算，扩展与明确的替代，并定义了一个组合输出为基础的解释到一个变种的π演算与配对，保留单步显式头减少弱双相似性。我们定义了四个概念的弱等价的Euda-mu-一个基于弱约化，两个建模弱头约化和弱显头约化（所有考虑没有弱头范式等价项），和一个基于弱近似-并显示它们都是一致的。然后，我们将展示完整的抽象结果，我们的解释弱等价弱双相似的过程。
2014-09-11 cs.LO
Deriving Abstract Semantics for Forward Analysis of Normal Logic Programs
虽然否定作为失败是通过内建谓词来处理的，但在文献中还没有正式地讨论{ \em normal}逻辑程序的前向抽象解释问题！在Prolog中实现的方式。本文提出了一个解决这个问题的方法，推导出两个通用的不动点抽象语义$F^b and $ F^ \diamond { \em正常}逻辑程序的前向抽象解释。$F^b$用于推断程序图中边的数据描述，其中边表示执行控制从其源程序点转移到其目的程序点的可能性。$F^\diamond$源自$F^b$，用于推断文本程序点的数据描述。
1998-11-06 cs.LO cs.PL
Interpolant Tree Automata and their Application in Horn Clause Verification
本文研究了凸多面体域上的抽象解释与插值树自动机相结合的Horn子句验证的抽象-精化方案。这些技术以前已经单独应用，但在本文中以一种新的方式相结合。内插树自动机的作用是在精化过程中提供一个伪反例的概括，捕获一组可能无限的伪反例迹。在我们的方法中，这些痕迹，然后消除使用的Horn子句的变换。我们比较这种方法与其他两种方法，其中之一使用插值树自动机的算法跟踪抽象和细化，而另一个使用抽象的解释没有概括步骤的凸多面体的域。一些霍恩子句验证问题的实验结果的评价表明，插值树自动机与抽象解释的组合给出了一些增加的验证工具的力量，而有时会产生的性能开销。
2016-07-10 cs.LO
Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
本文提出一种扩展一阶逻辑，以 Hoare 三元组风格对抽象状态进行推理，并通过可实现性解释将证明提取为混合函数式/命令式程序，同时给出基于状态单子的语义解释及 Heyting 算术单子扩展。
2024-01-25 cs.LO math.LO
Categorical Vector Space Semantics for Lambek Calculus with a Relevant Modality (Extended Abstract)
我们开发了一个有相关模态的Lambek演算的分类成分分布语义，它具有有限版本的压缩和排列规则。语义学的范畴部分是一个monoidal双闭范畴，其上有一个定义在微分范畴上的余代数模态。我们实例化这一类有限维向量空间和线性映射，通过量化函子和工作与三个具体的解释的余代数模态。我们应用该模型来构建分类和具体的语义解释的动机的例子，这个扩展演算：派生的短语与寄生的差距。具体解释的有效性通过消歧任务进行评估，在将句子消歧数据集扩展到寄生间隙短语上，使用BERT，Word2Vec和FastText向量和关系张量
2021-01-26 cs.LO
Invariant stream generators using automatic abstract transformers based on a decidable logic
在模型或源代码上使用形式化分析工具通常需要关于所研究系统的辅助不变量的可用性。抽象解释是目前发现有用的不变量，特别是数值不变量的最佳方法之一。然而，它的应用受到两个正交问题的限制：（i）开发抽象解释通常是不平凡的;系统的每个传递函数必须在抽象级别上表示，这取决于所使用的抽象域;（ii）对于精确但昂贵的抽象域，由抽象解释器计算的信息只能在到达后定点时使用;这对于非常大的系统分析可能需要很长时间，或者延迟加宽以提高精度。本文提出了一种新的，完全自动的，方法来建立抽象解释器。它的一个很好的特点是，它产生的解释器可以提供声音的不变量的分析系统到达后固定点计算结束之前，所以作为在飞行不变的发电机。
2012-05-16 cs.LO cs.SE
Graph Subsumption in Abstract State Space Exploration
在本文中，我们提出了一个现有的方法的扩展抽象图为基础的状态空间探索，称为邻域抽象，减少技术的基础上包容。基本上，当一个抽象的状态覆盖了更多的具体状态时，它就包含了另一个抽象的状态;在这种情况下，被包含的状态不需要包含在状态空间中，从而给出了一个约简。我们解释的理论，特别是还报告了一些实验，这表明包容确实大大减少了状态空间和计算它所需的资源（时间和内存）。
2012-10-24 cs.LO
An intensionally fully-abstract sheaf model for $π$ (expanded version)
本文为 $\pi$-演算提出基于简单站点上层的组合模型，该层对应并发无辜策略，并证明其内涵完全抽象于公平测试等价，核心是借助字符串图构造站点。
2017-11-14 cs.LO cs.PL
A Control Flow based Static Analysis of GRAFCET using Abstract Interpretation
针对GRAFCET并发行为易导致状态空间过大的问题，提出基于抽象解释的控制流静态分析方法，可检查无并发实例并开展流敏感分析，经工业级示例验证有效。
2023-08-25 cs.LO cs.PL cs.SY
Categorical Abstract Rewriting Systems and Functoriality of Graph Transformation
重写系统通常被定义为给定对象集上的二元关系。这个简单的定义被用来描述重写的各种属性，如终止，合流，范式等。在本文中，我们引入了一个新的概念，抽象重写范畴的框架。然后，我们定义了重写系统的函性性质。这种特性有时称为垂直合成。我们表明，大多数图变换系统是函的，并提供了一个反例的图变换系统，这是不是函的。
2011-05-31 cs.LO
Responsibility Analysis by Abstract Interpretation
给定程序中感兴趣的行为，静态地确定相应的责任实体是至关重要的任务，特别是在程序安全性方面。经典的静态分析技术（例如依赖性分析、污点分析、切片等）帮助程序员缩小责任范围，但他们都不能明确地确定责任实体。同时，因果关系分析一般不适用于程序的分析，而结构方程模型（SEM）的实际因果关系忽略了程序固有的一些信息，使得其对程序的分析不精确。本文提出了一种新的基于事件跟踪语义抽象的责任定义，该定义可应用于程序安全等科学领域。简单地说，实体ER负责行为B，当且仅当ER可以自由选择其输入值，并且这样的选择是确保B在即将到来的执行中出现的第一个选择。与现有的分析方法相比，责任分析更加精确。此外，我们对责任的定义考虑了观察者的认知，据我们所知，这是程序分析中的一个新的创新思想。
2019-07-18 cs.LO cs.PL
Making Abstract Domains Condensing
在本文中，我们表明，可逆分析的逻辑语言的抽象解释可以进行不损失的精度，系统地细化抽象域。其思想是将语义结构包含到抽象域中，以这种方式，精炼的抽象域变得足够丰富，以允许近似的自底向上和自顶向下语义一致。这些域被称为压缩抽象域。实质上，如果目标驱动和目标独立分析一致，则抽象域是浓缩的，即在目标独立分析中近似查询不会引起精度损失。我们证明了凝聚是一个抽象的域属性，并使一个抽象域凝聚的问题归结为问题，使域完整的统一。在一般的抽象解释设置，我们表明，当具体的域和操作引起quantales，即模型的命题线性逻辑，对象在一个完整的精炼抽象域可以明确的特征在于线性逻辑为基础的配方。这是用于逻辑程序分析的抽象域的情况，近似计算的答案替换，其中统一在幂等替换的Quantale中扮演乘法合取的角色。因此，凝聚抽象域可以通过最小限度地扩展任何，通常非凝聚域，由一个简单的域细化算子系统地得出。
2002-04-09 cs.LO cs.PL
Computing and Proving Well-founded Orderings through Finite Abstractions
检查复杂状态机属性的常用技术是构建一个有限抽象，然后检查抽象系统上的属性--如果抽象被证明是代表性的，则仅将对抽象系统的通过检查转移到原始系统。这种方法确实需要有限抽象的推导或定义，但可以避免复杂的不变量定义的需要。为了检查微处理器中内存事务的进程，我们需要证明复杂状态机中的事务总是进展到完成。作为这项工作的一部分，我们开发了一个过程，用于计算目标状态机的有限抽象图，以及关于抽象图中的弧上的某些度量是否减少的注释。然后，我们迭代地将抽象图分成强连接的组件，然后为抽象图中的每个节点建立一个度量，确保在原始系统的每个过渡中减少，以保证进度。对于有限状态的目标系统（如硬件设计），我们提出了有效地提取抽象图的方法，使用增量SAT通过GL，然后应用我们的过程来检查进展。我们提出了一个实现的面包店算法作为一个例子应用程序。
2020-09-29 cs.LO
Convergence in Infinitary Term Graph Rewriting Systems is Simple (Extended Abstract)
在这个扩展的摘要中，我们提出了一个简单的方法来收敛项图，使我们能够统一项图重写和无穷项重写。这种方法是基于偏序和度量的术语图。这些结构是无穷项重写中使用的相应结构的简单概括。我们将我们的简单方法与我们之前开发的更复杂的方法进行比较，并表明这种新方法在许多方面都更优越。唯一不利的财产，我们能够确定，即失败的弱度量和偏序收敛之间的充分对应，是通过采用强收敛纪律纠正。
2013-02-26 cs.LO cs.PL
Über die Präzision interprozeduraler Analysen
在这项工作中，我们研究了两种方法来分析Sharir和Pnueli在精度方面的过程间数据流：函数和调用字符串的方法。在这样做时，不仅理论上最好的，但所有的解决方案都被认为是使用抽象的解释或扩大时发生的。事实证明，这两种方法的解决方案是一致的。当使用抽象解释时，这个属性会被保留;在扩大的情况下，结果的比较并不总是可能的。
2017-03-29 cs.LO cs.PL
Ascertaining Uncertainty for Efficient Exact Cache Analysis
静态缓存分析通过以合理但近似的方式确定哪些内存访问导致缓存命中以及哪些导致缓存未命中来表征程序的缓存行为。这些信息在优化编译器、最坏情况下的执行时间分析以及侧信道攻击量化和缓解方面都是有价值的。高速缓存分析通常作为“必须”和“可能”抽象解释的组合来执行，将指令分类为“总是命中”、“总是未命中”或“未知”。分类为“未知”的指令可能会导致命中或未命中，这取决于程序输入或初始高速缓存状态。同样可能的是，它们实际上总是命中或总是未命中，但是高速缓存分析太粗糙而看不到它。我们消除这种不确定性的方法包括（i）一种新颖的抽象解释，能够确定特定指令肯定会在不同路径上导致命中和未命中，以及（ii）一种精确的分析，基于模型检验，消除所有剩余的不确定性，使用抽象解释结果来修剪模型的可扩展性。我们在各种示例上评估了我们的方法;它以合理的成本显着提高了经典抽象解释的精度。
2018-12-20 cs.AR cs.LO cs.PL
