Delay-Bounded Scheduling Without Delay! (Extended Technical Report)
我们认为，在任意线程交织的异步并发程序的安全性分析的广泛问题。延迟有界的确定性调度，介绍了在以前的工作中，是一个有效的错误发现技术，以遏制与充分的调度不确定性的大成本。在本文中，我们首先提出了一种技术，以解除有限域变量程序的情况下的延迟界，从而增加了效率的错误检测的能力，证明安全的程序在任意线程交织。其次，我们展示了如何，结合谓词抽象，我们的技术可以反驳和验证安全属性的程序与无界的变量域，即使是无限的线程数。以前的工作已经建立，对于非平凡的并发例程，谓词抽象诱导一个高度复杂的抽象程序语义。然而，我们的技术，从来没有静态地构造一个抽象的参数化程序，它只需要一些抽象状态集在某些行动下被关闭，从而消除了对存在的抽象程序的验证算法的依赖。我们证明了我们的技术在以前的工作中使用的许多例子的效率，并展示其简单性相比，早期的方法在无限线程票锁协议。
2021-05-15 cs.PL
Modular GPU Programming with Typed Perspectives
针对GPU编程中线程级控制与集体操作协同的冲突导致模块化代码易出错的问题，提出带类型化视角的GPU语言Prism，可在不损失性能的前提下保障模块化编程的安全性。
2025-11-14 cs.DC cs.PL
A Model of Cooperative Threads
我们开发了一个模型的并发命令式编程线程。我们专注于一个小的命令式语言与合作的线程，执行无中断，直到他们终止或显式地产生控制。我们定义并研究了这种语言的基于跟踪的指称语义，这种语义是完全抽象的，但数学上是初等的。我们还给出了一个方程理论的计算效果，基础的语言，包括线程产卵。然后，我们分析线程的自由代数单子这个理论。
2010-10-20 cs.PL
A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs
无数据竞争程序是一类重要的并发程序。在本文中，我们提供了一个框架，设计和证明的正确性数据流分析，针对这一类的程序。这些分析与早期文献中提出的“同步-CFG”分析具有相同的精神。为了实现这一点，我们首先提出了一种新的具体语义DRF程序，称为L-DRF，这是线程本地的性质-每个线程操作自己的副本的数据状态。我们表明，我们的语义抽象，使我们能够减少DRF程序的分析，顺序分析。这有助于将现有的顺序分析快速移植到DRF程序的合理和可扩展的分析中。接下来，我们将L-DRF参数化，将程序变量划分为原子访问的“区域”。区域参数化语义的抽象产生更精确的分析“区域种族”自由并发程序。我们实例化这些抽象设计高效的关系分析种族自由的程序，我们已经实现了一个原型工具，称为RATCOP。在基准测试中，RATCOP能够证明高达65%的断言，相比之下，我们的基线证明了25%。此外，在与最近的并发静态分析器的比较研究中，RATCOP快了5个数量级。
2020-09-06 cs.PL
Thread-Modular Static Analysis for Relaxed Memory Models
提出了一种内存模型感知的静态程序分析方法，用于精确分析运行在具有弱一致性模型（如x86-TSO、SPARC-PSO和SPARC-RMO）的处理器上的并发软件的行为。在我们的方法的中心是一个统一的框架，用于决定线程间干扰的可行性，以避免传播虚假的数据流在静态分析，从而提高静态分析器的性能。我们制定的检查干扰的可行性作为一组数据库规则，这是有效的解决和一般足以捕捉一系列的硬件级内存模型。与现有技术相比，我们的方法可以显着减少虚假警报的数量，以及不健全的证据。我们实现了该方法，并评估了一个大的多线程的C程序集。我们的实验表明，该方法显着优于国家的最先进的技术在准确性方面只有适度的运行时开销。
2017-09-28 cs.PL cs.SE
On Modular and Fully-Abstract Compilation -- Technical Appendix
安全编译研究生成与源级别组件一样安全的目标级别组件的编译器。在定义安全编译器时，完全抽象是得到最广泛证明的属性。一个编译器是模块化的，如果它允许不同的组件独立编译，然后连接在一起形成一个完整的程序。不幸的是，许多现有的非类型化机器码的完全抽象编译器不是模块化的。因此，虽然完全抽象的编译组件对于恶意攻击者来说是安全的，但如果它们相互链接，那么生成的组件可能会变得容易受到攻击。本文研究如何设计模块化的、完全抽象的编译器。它首先分析了编译程序链接在一起时产生的攻击，确定了由于链接造成的安全威胁。然后，它定义了一个编译器，从一个基于对象的语言与方法调用和动态内存分配，以非类型化的汇编语言扩展与内存隔离机制。本文提供了一个证明草图，所定义的编译器是完全抽象和模块化的，所以它的输出可以连接在一起，而不会引入安全违规。
2016-04-18 cs.PL
From Single-thread to Multithreaded: An Efficient Static Analysis Algorithm
现在已经开发了各种各样的计算单线程程序安全性的静态分析。本文提出了一个系统的方法来扩展一类这样的静态分析，使他们处理程序与多个POSIX风格的线程。从语用操作语义学出发，我们建立了一个指称语义，表示推理的一个假设保证。最后的算法，然后通过抽象的解释。它依次分析每个线程，传播线程之间的干扰以及其他语义信息。组合爆炸，随之而来的明确考虑的所有交织，从而避免。与单线程情况相比，最坏情况的复杂度仅增加了n倍，其中n是程序中的指令数。我们已经实现了原型工具，证明了该方法的实用性。
2009-10-30 cs.PL
Towards Cumulative Abstract Semantics via Handlers
University of Colorado Boulder（科罗拉多大学博尔德分校）；Amazon（亚马逊）
本文提出通过作用域效应实现累积抽象语义，以构建模块化且优雅的抽象解释框架。
2026-02-17 cs.PL
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)
本文提出一种基于幽灵的并发程序正确性见证格式，使交错语义与线程模块化语义下的见证有效性一致，并在SV-COMP基准上验证了其可行性。
2024-11-25 cs.PL
Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs
我们提出了一个静态分析的抽象解释检查运行时间错误的并行和多线程的C程序。在我们的工作Astrée，我们专注于嵌入式关键程序没有递归，也没有动态内存分配，但扩展到一个静态的线程集的分析，通过共享内存和显式地使用一组有限的互斥锁隐式通信，并根据实时的【形】调度策略和固定的优先级调度。我们的方法是线程模块化的。它是基于一个稍微修改的非平行分析，当分析一个线程，应用和丰富的一组抽象的线程冲突。然后迭代器依次重新分析每个线程，直到冲突稳定下来。我们证明了我们的方法的可靠性顺序一致性语义，但也相对于一个合理的弱一致的内存语义。我们还展示了如何考虑互斥和线程优先级，通过分区的抽象调度状态。我们展示了使用原型Thésée分析工业程序的初步实验结果，并展示了我们方法的可扩展性。
2012-03-22 cs.LO cs.PL
Data Race Detection by Digest-Driven Abstract Interpretation (Extended Version)
本文提出通过摘要驱动的抽象解释方法，结合锁集摘要和线程ID推理，显著提升数据竞争检测的准确性。
2025-11-25 cs.PL cs.SE
Modular abstract syntax trees (MAST): substitution tensors with second-class sorts
University of Cambridge（剑桥大学）；University of Edinburgh（爱丁堡大学）；University of Innsbruck（因斯布鲁克大学）；University of Oxford（牛津大学）
本文提出模块化抽象语法树（MAST）理论，通过双范畴论方法研究具有第二类排序的语言，证明CBV的替代引理。
2026-02-27 cs.PL
Modular Abstractions of Reactive Nodes using Disjunctive Invariants
我们希望将反应式程序设计语言（如Lustre）中的节点抽象为具有更简单控制结构的节点，并限制控制状态的数量。为了做到这一点，我们在谓词抽象中计算析取不变量，其中有有限数量的析取，然后我们抽象节点，每个析取代表一个抽象状态。析取不变量的计算是通过使用SMT求解表示的量词消去的形式来执行的。同样的方法也可以用来获得析取循环不变量。
2011-09-09 cs.LO cs.PL
Galois Transformers and Modular Abstract Interpreters
静态分析器的设计和实现已经变得越来越系统化。然而，对于一个给定的语言或分析功能，它往往需要繁琐和容易出错的工作，以实现分析器，并证明它的声音。简而言之，静态分析特性和它们的可靠性证明不能很好地组合，导致在实现和元理论中缺乏重用。我们通过引入伽罗瓦变换器解决了系统地构建静态分析器的问题：单子变换器传输伽罗瓦连接属性。与一个单子解释器相配合，我们定义了一个单子转换器库，这些转换器实现了经典分析参数（如上下文、路径和堆（入）敏感性）的构建块。此外，这些可以独立于被分析的语言组合在一起。重要的是，Galois Transformer可以被证明是可靠的，使其成为可重用的分析组件。随着新的分析特征和抽象的开发和混合，可靠性证明不需要重建，因为单子Transformer堆栈的组成凭借其成分是可靠的。伽罗瓦变换为程序分析的可重用和可组合元理论提供了一个可行的基础。最后，这些伽罗瓦变换器将分析设计和实现中的抽象级别转移到非专业人员能够在多个参数上合成声音分析器的级别。
2015-10-05 cs.PL
Automatic Modular Abstractions for Linear Constraints
提出了一种通过抽象解释自动生成用于静态分析的抽象Transformers的方法。该方法的重点是对程序的线性约束，操作合理的，真正的或浮点变量，并包含线性分配和测试。除了无循环代码，同样的方法也适用于获得最小不动点作为前提条件的函数，这允许分析循环和递归函数。我们的算法是基于新的量词消去和符号操作技术。给定一个抽象域的规范和一个程序块，我们的方法自动输出相应的抽象Transformer的实现。因此，它是程序转换的一种形式。我们工作的动机是数据流同步程序设计语言，用于构建控制命令嵌入式系统，但它也适用于命令式和函数式编程。
2008-11-02 cs.LO cs.PL
Automatic modular abstractions for template numerical constraints
提出了一种通过抽象解释自动生成用于静态分析的抽象Transformers的方法。该方法的重点是对程序的线性约束，操作合理的，真正的或浮点变量，并包含线性分配和测试。除了无循环代码，同样的方法也适用于获得最小不动点作为前提条件的函数，这允许分析循环和递归函数。我们的算法是基于新的量词消去和符号操作技术。给定一个抽象域的规范和一个程序块，我们的方法自动输出相应的抽象Transformer的实现。因此，它是程序转换的一种形式。我们工作的动机是数据流同步程序设计语言，用于构建控制命令嵌入式系统，但它也适用于命令式和函数式编程。
2010-05-31 cs.LO cs.PL
Modular, Fully-abstract Compilation by Approximate Back-translation
本文提出通过近似反向翻译技术，解决源语言表达能力不足时编译器完全抽象性证明的难题，并在STLC到ULC编译器上实现首个Coq机械化证明。
2017-10-24 cs.PL
An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
University of Edinburgh（爱丁堡大学）；University of Oxford（牛津大学）
本文通过代数效应为动态线程提供等式公理化，结合参数化代数理论构建并发编程语言的语义模型。
2026-02-05 cs.PL
Automatic Modular Abstractions for Template Numerical Constraints
提出了一种通过抽象解释自动生成用于静态分析的抽象Transformers的方法。该方法的重点是对程序的线性约束，操作合理的，真正的或浮点变量，并包含线性分配和测试。给定一个抽象域的规范和一个程序块，我们的方法自动输出相应的抽象Transformer的实现。因此，它是程序转换的一种形式。除了无循环代码，同样的方法也适用于获得最小不动点作为前提条件的函数，这允许分析循环和递归函数。我们工作的动机是数据流同步程序设计语言，用于构建控制命令嵌入式系统，但它也适用于命令式和函数式编程。我们的算法是基于线性算术公式上的量词消去和符号操作技术。我们也给出了非线性约束和非线性程序结构的一般结果。
2010-05-26 cs.LO cs.PL
Operational Aspects of C/C++ Concurrency
在这项工作中，我们提出了一个家庭的操作语义，逐渐接近现实的程序行为的C/C++11内存模型。我们框架中的每个语义都是通过阐述和组合两个简单的成分构建的：视图和操作缓冲区。视图允许我们表达线程交互的空间方面，即，线程可以读取哪些值，而操作缓冲器使得能够利用时间执行方面进行操纵，即，确定某些操作的结果可以被并发运行的线程观察到的顺序。从一个简单的抽象状态机开始，通过一系列的抽象状态的逐步细化，我们捕获这样的语言方面和同步原语的释放/获取原子，顺序一致和非原子内存访问，还提供了一个语义放松原子，同时避免了稀薄空气的问题。据我们所知，这是C11的第一个正式的和可执行的操作语义，能够表达标准的所有基本并发方面。我们说明了我们的方法，通过一些特征的例子，有关观察到的行为，从文献中的标准石蕊测试程序。我们提供了一个可执行的PLT Redex中的语义实现，以及一些实现的石蕊测试和示例，并展示了我们的原型上的一个大型案例研究：随机测试和调试一个现实的读取-复制-更新数据结构。
2016-07-09 cs.PL
Correctness Witness Validation by Abstract Interpretation
本文提出一种新颖的抽象操作 unassume，通过将见证不变式纳入抽象程序状态以加速不动点收敛并提升精度，实现了通过抽象解释验证正确性见证，显著减少了多线程程序验证的 CPU 时间并能验证原本无法验证的属性。
2023-10-25 cs.PL
Deriving Escape Analysis by Abstract Interpretation: Proofs of results
面向对象语言的逃逸分析近似于不从给定上下文逃逸的对象集。如果我们把一个方法作为上下文，非转义对象可以在它的激活堆栈上分配;如果我们把一个线程作为上下文，那么就不需要在这些对象上使用Java同步锁。在本文中，我们形式化的基本逃逸域E作为一个抽象的解释具体的国家，我们然后细化到一个抽象的域ER比E更具体，因此，导致更精确的逃逸分析比E。我们提供的最优性结果为E和ER，在形式的伽罗瓦插入从具体的抽象域和最佳的抽象操作。伽罗瓦插入属性是通过使用抽象垃圾收集器将抽象域限制为不包含垃圾的那些元素而获得的。因此，我们实现的er是一个正式正确的转义分析器的实现，能够检测Java（字节码）应用程序的堆栈可分配创建点。这份报告包含了一篇论文的结果的证明，该论文具有相同的标题和作者，并将发表在《高阶符号计算》杂志上。
2006-07-28 cs.PL
Modular Construction of Shape-Numeric Analyzers
静态分析的目的是推断程序的不变量，这些不变量足够精确以建立语义属性，例如不存在运行时错误。一般来说，命令式程序的静态分析有两个主要分支。指针和形状分析侧重于推断指针、动态分配的内存和递归数据结构的属性，而数值分析则寻求导出数值的不变量。虽然通常需要同时推断形状-数值不变量，但这种情况特别具有挑战性，并且没有得到特别好的探索。值得注意的是，同时的形状-数值推理在静态分析器本身的设计中提出了复杂的问题。在本文中，我们研究的建设，这样的形状数值，静态分析。我们建立了一个抽象的解释框架，使我们能够推理的形状和数字的抽象组合成一个模块化的，富有表现力的抽象域的同时形状数值属性。这种模块化结构是非常可取的，使其形式化和实现更容易做，并得到正确的。为了实现这一点，我们选择了一个具体的语义，可以一步一步地抽象，同时保持高水平的表达能力。抽象操作的结构（即，transfer、join和comparison）遵循该语义的结构。这种构造的优点是将分析器划分为模块和函数，这些模块和函数实现了不同特性的抽象。
2013-09-20 cs.LO cs.PL
Safety Verification of Parameterized Systems under Release-Acquire
研究了参数化系统在发布-获取语义下的安全性验证问题。已经表明，对于具有对原子比较和交换（CAS）指令的无限访问的系统，该问题是棘手的。我们表明，从验证的角度来看，近似结果的帮助，这是过于悲观。我们研究参数化系统组成的无限数量的环境线程执行相同的，但CAS免费的程序和一个固定数量的区别线程是不受限制的。我们的第一个贡献是一个新的语义，大大简化了RA，但仍然相当于上述系统的安全验证。我们将这个（一般）结果应用于我们模型的两个子类。我们表明，安全验证是唯一的\pspace-完成的有界模型检验问题的区别线程是无循环的。有趣的是，我们仍然可以负担无限的环境。我们表明，复杂性跳转到\nexp-完成线程模块化验证，其中一个不受限制的区别'自我'线程与环境的CAS-自由线程加循环区分线程（如在前面的设置）。除了验证的有用性，结果是强大的，因为它们划定了一个既定的语义的易处理性边界。
2022-05-05 cs.LO cs.PL
Abstract Interpretation with Unfoldings
我们提出并评估了一种技术，用于计算路径敏感的并发程序的抽象解释过程中的干扰条件。代替不动点计算，我们使用素事件结构来compensate表示因果关系的依赖性和干扰之间的序列的变压器。我们的主要贡献是一个展开算法，使用一个新的概念的独立性，以避免冗余的Transformer应用程序，线程本地固定点，以减少展开的大小，和一个新的截断标准的基础上包容，以保证终止的分析。我们的实验表明，抽象展开产生一个数量级的假警报比一个成熟的抽象解释器，而几个数量级的速度比求解器为基础的工具，具有相同的精度。
2017-05-01 cs.LO cs.PL
Modular Labelled Sequent Calculi for Abstract Separation Logics
抽象分离逻辑是霍尔逻辑的一系列扩展，用于推理操纵诸如存储器位置之类的资源的程序。这些逻辑是“抽象的”，因为它们独立于任何特定的具体资源模型。他们的断言语言，称为命题抽象分离逻辑（PASL），以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。特别地，这些逻辑包含连接词$*$和$-\!*$，分别表示资源的组成和扩展。这种额外的表达能力是有代价的，因为所产生的逻辑都是不可判定的。鉴于其广泛的适用性，甚至半决策程序，这些逻辑是可取的。虽然在文献中讨论了几个PASL和它们与BBI的关系，但这些逻辑的证明理论和自动推理是本文的会议版本解决的开放问题，该版本使用无割标记演算为各种PASL开发了模块化证明理论。本文非平凡地改进了以前的工作，给出了一个一般框架的演算上的任何新的公理在逻辑满足一定的形式对应的推理规则在我们的框架，和完整性证明一般考虑这样的公理。我们的基础演算处理Calcagno等人。的原始逻辑的分离代数，增加了健全的规则，部分确定性和cancellativity，同时保持削减消除。然后，我们证明了分离逻辑中的许多重要性质，如不可分单元、不相交性、可分裂性和交叉分裂性，都可以用我们的一般公理形式表示。因此，我们的框架免费提供了这些属性的推理规则和完整性。最后，我们展示了我们的演算如何减少到具有全局标签替换的演算，从而实现更高效的实现。
2018-03-26 cs.LO cs.PL
A Few Graph-Based Relational Numerical Abstract Domains
本文给出了一类非关系数值抽象域的系统设计。构造的域表示形式为（C中的vj - vi）的不变量的集合，其中vj和vi是两个变量，并且C存在于P（Z）、P（Q）或P（R）的抽象中。我们称这类域为弱关系域。允许这种建设的基本概念是潜在的图形和最短路径封闭算法在exotic-like代数的扩展。给出了示例构造，以检索知名的域以及新的。这样的域可以在抽象解释框架中使用，以便设计各种静态分析。这种结构的一个主要好处是它的模块化，允许快速实现新的抽象域从现有的。
2007-03-16 cs.PL
RacerF: Lightweight Static Data Race Detection for C Code
本文提出RacerF，一种基于Frama-C平台的轻量级静态分析工具，通过上下近似方法实现线程模块化数据竞争检测，在保证高精度的同时提升检测速度。
2025-06-18 cs.PL cs.SE
Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis
Universidad Politécnica de Madrid（马德里理工大学）；IMDEA Software Institute（IMDEA软件研究所）；Spanish Council for Scientific Research (CSIC)（西班牙国家研究委员会）；Computer Science Laboratory of Sorbonne University (LIP6)（索邦大学计算机科学实验室）；STMicroelectronics（意法半导体）
该研究提出算子语义与抽象编译框架，将其应用于静态代价分析，开发出支持通用函数未知量等的最优递归提取技术，提升了代价分析的可靠性与精确性。
2026-08-11 cs.LO cs.PL
An Experiment Combining Specialization with Abstract Interpretation
以前的研究表明，控制流细化可以通过一个程序专门化结合基于属性的抽象来实现，以提高终止和复杂性分析工具。我们现在表明，这个专门构建的专门化程序可以以更模块化的方式进行重构，并且可以使用现成的部分评估工具来实现先前的结果，并将其应用于抽象解释器。抽象解释器的关键特征是抽象域，它是基于属性的抽象域与具体域的乘积。这种独立于语言的框架提供了一种实用的方法来实现各种强大的专门化，并有助于使用解释器和专门化来实现程序转换的研究。
2020-08-07 cs.LO cs.PL cs.SC
