RustHorn: CHC-based Verification for Rust Programs (full version)
约束Horn子句的可满足性问题约简是一种被广泛研究的自动程序验证方法。然而，目前基于CHC的指针操作程序方法的可扩展性不是很好。本文提出了一种将指针操作Rust程序转换为CHC的新方法，该方法通过利用所有权来清除指针和内存。我们形式化了Rust的简化核心的翻译，并证明了它的正确性。我们已经为Rust的一个子集实现了一个原型验证器，并证实了我们方法的有效性。
2020-06-11 cs.PL
Reductions for Safety Proofs (Extended Version)
程序归约被广泛用于简化并发和分布式程序正确性的推理。在本文中，我们提出了一个通用的方法来证明简化的并发程序的基础上探索通用类的减少。我们介绍了两类健全的程序减少，研究其理论特性，显示它们如何可以有效地用于算法验证，并证明它们是非常有效的生产证明的不同类别的程序，而不针对这些程序的特定语法属性。本文最新颖的贡献是在程序约简的定义中引入了上下文的概念。我们演示了如何在某些程序的上下文中的程序步骤的可交换性可以用来定义一个通用类的声音减少，可以用来自动产生证明程序的完整的Floor-Hoare风格的证明理论上超出了今天的自动验证技术。
2019-10-31 cs.PL
Symbolic Semantics for Probabilistic Programs (extended version)
本研究基于Kozen的工作提出含observe语句与连续分布采样的概率程序的新型符号执行语义，完成正确性证明，在symProb工具中实现并通过示例验证。
2023-07-19 cs.PL
Petrification: Software Model Checking for Programs with Dynamic Thread Management (Extended Version)
本文针对动态 fork/join 线程的并发程序验证，提出 petrification 转换，将其归约为基于 Petri 网的固定线程数形式化体系，并在支持 pthreads 的 C 程序模型检测工具中实现。
2023-11-02 cs.PL
DisQ: A Model of Distributed Quantum Processors (Extended Version)
University of Maryland（马里兰大学）；Iowa State University（爱荷华州立大学）
本文提出DisQ模型，结合化学抽象机与马尔可夫决策过程，为分布式量子处理器提供清晰的并发与分布式行为区分，并开发模拟关系验证量子算法与分布式版本等价性。
2026-04-03 cs.PL quant-ph
Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
RWTH Aachen University（亚琛工业大学）
本文提出一种简单程序化方法，通过增量差异分析概率程序的多种目标，如高矩、阈值概率等，利用现有推理方法实现统一分析。
2026-03-02 cs.PL
Gobra: Modular Specification and Verification of Go Programs (extended version)
Go是一种越来越流行的系统程序设计语言，特别是针对并发和分布式系统。Go语言与其他命令式语言的不同之处在于，它通过goroutine提供了结构化的子类型和轻量级的并发性以及消息传递通信。这些特性的组合为静态验证提出了有趣的挑战，最突出的是可变堆和高级并发原语的组合。我们提出Gobra，一个模块化的，演绎的程序验证器，证明内存安全，崩溃安全，数据竞争自由，和用户提供的规范。Gobra基于分离逻辑，支持Go语言的一个大子集。它的实现将带注释的Go程序转换为Viper中间验证语言，并使用现有的基于SMT的验证后端来计算和履行证明义务。
2021-05-28 cs.PL
Version Space Algebras are Acyclic Tree Automata
版本空间代数是一种表示程序空间的方法，可以使用并集、交集和叉积/"连接”运算符来组合。在其具体形式为具有显式联合和连接节点的AST中，它们具有压缩表示指数大空间的程序的能力，因此它们已成为自2010年引入FlashFill以来最流行的枚举程序合成方法。我们提出了一个从版本空间代数到非确定有限树自动机的线性时间语义保持的构造嵌入，表明前者只是后者的一个特例。结合最近的结果发现之间的对应关系的e-图和最小的确定性树自动机，这表明树自动机是严格的概括最近所有的主要方法，有效地表示大空间的程序共享。
2021-07-27 cs.PL
Synthesizing Database Programs for Schema Refactoring
许多与数据库交互的程序在其生存周期中需要经历多次模式重构。由于这个过程通常需要对程序的实现进行重大更改，因此模式重构通常是不平凡的，并且容易出错。出于这个问题，我们提出了一种新的技术，自动合成一个新版本的数据库程序给定其原始版本和源和目标模式。我们的方法不需要人工用户的指导，并确保合成的程序是相当于原来的。此外，我们的方法是相当有效的，可以合成新版本的数据库程序（包含多达263个功能），从现实世界的Web应用程序中提取的平均合成时间为69.4秒。
2019-04-11 cs.PL
A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs -- Extended Version --
定义了一种简单的动态类型、（纯粹的）面向对象语言。给出了一种结构化的操作语义和一种Hoare式的程序逻辑，用于在多个正确性概念中对语言中的程序进行推理。霍尔逻辑被证明是合理的和（相对）完整的，是-尽我们所知-第一个这样的逻辑动态类型的语言。
2016-01-08 cs.LO cs.PL
N-Version Obfuscation: Impeding Software Tampering Replication with Program Diversity
防篡改是软件安全的一个重要研究领域。已经提出了许多方法来阻止特定的篡改过程，例如，混淆和自校验和。然而，据我们所知，它们都不能达到理论上的防篡改。我们的想法是通过程序的多样化来阻止篡改的复制，从而增加破解整个软件系统的复杂性。为此，我们建议提供相同的功能，但功能不等同的软件副本到不同的机器。我们正式定义的问题N版本混淆，并提供了一个可行的手段来解决这个问题。我们的评估结果表明，打破软件系统所需的时间是线性增加的软件版本的数量，这是O（n）的复杂度。
2015-06-08 cs.CR cs.PL
Failure-Directed Program Trimming (Extended Version)
本文介绍了一种新的程序简化技术，称为程序修剪，旨在提高安全检查工具的可扩展性和精度。给定程序${\mathcal P}$，程序修整生成新程序${\mathcal P}'$，使得${\mathcal P}$和${\mathcal P}'$是同等安全的（即，${\mathcal P}'$有bug当且仅当${\mathcal P}$有bug时），但${\mathcal P}'$的执行路径比${\mathcal P}$少。由于许多程序分析器是敏感的执行路径的数量，程序修剪有可能提高安全检查工具的有效性。除了引入程序修剪的概念，本文还提出了一个轻量级的静态分析，可以作为一个预处理步骤，删除程序路径，同时保持等安全性。我们已经实现了所提出的技术在一个工具，称为修剪和评估它的上下文中的两个程序分析技术，即抽象解释和动态符号执行。我们的实验表明，程序修剪显着提高了这两种技术的有效性。
2017-06-14 cs.PL cs.SE
Program Equivalence for Assisted Grading of Functional Programs (Extended Version)
在涉及编程作业的课程中，给学生有意义的反馈是一个重要的挑战。人类可以通过手动评分程序来提供有用的反馈，但这是一个耗时，劳动密集型，并且通常无聊的过程。自动评分器速度快，可扩展性好，但它们通常提供的反馈很差。虽然已经有关于改进自动分级机的研究，但是关于缩放和改进人类分级的研究是有限的。我们建议通过使用等价算法来增强手动评分过程，该算法可以识别学生提交文件之间的等价关系，从而扩展人工评分。这使人类评分员能够一次为多个学生提交的内容提供有针对性的反馈。我们的技术在两个方面是保守的。首先，它识别算法相似的提交之间的等效性，例如，它不能识别快速排序和合并排序之间的等价性。其次，它使用正式的方法，而不是聚类算法从机器学习文献。这使我们能够证明一个可靠的结果，保证提交永远不会错误地聚集在一起。尽管只有报告等价时，有算法的相似性和正式证明等价的能力，我们表明，我们的技术可以显着减少评分时间从介绍函数编程课程的数千个编程提交。
2020-10-15 cs.PL
Interpreting Knowledge-based Programs (Extended Version with Proofs)
知识为基础的程序指定多代理协议与认识的警卫，从代理如何学习和记录的事实或其他代理和环境的信息抽象。他们的解释涉及到一个非单调的相互依赖性之间的评价认识警卫的可达状态和推导的可达状态取决于评价认识警卫。我们申请的技术必须/不能分析发明的同步程序设计语言的解释问题的知识为基础的程序，并证明所产生的建设性的解释是单调的，有一个最小的不动点。我们将我们的方法与现有的解释计划同步和异步程序。最后，我们描述了一个建设性的解释，并说明了几个例子和应用程序的Java内存模型的过程。
2023-01-25 cs.LO cs.PL
Type-Preserving Flow Analysis and Interprocedural Unboxing (Extended Version)
过程间流分析可以用来消除不必要的堆分配对象（拆箱），在以前的工作中，我们已经展示了如何在保持垃圾收集器正确性的同时做到这一点。在本文中，我们扩展了流分析的概念，将类型，使类型化程序的分析和优化。我们应用这种类型化的分析，指定一个类型保持过程间拆箱优化，并证明优化保持类型和GC安全以及程序语义。我们还表明，拆箱优化可以独立地适用于单独编译的程序模块，并证明通过上下文等价的结果，拆箱隔离模块保留程序语义。
2012-03-09 cs.PL
The Complexity of Interaction (Long Version)
在本文中，我们分析了复杂的功能程序编写的交互网络计算模型，异步，并行和融合模型，概括线性逻辑证明网。采用用户定义的大小和预定的类型，我们证明了具体的时间，空间和空间-时间复杂度界限的顺序和并行减少的交互网络程序通过适当分配复杂性潜力的类型节点。原型编程的例子说明了这种方法的相关性。所提供的分析是精确的，组合的，并且在理论上不限于特定的复杂性类。
2015-11-05 cs.PL
Fencing off Go: Liveness and Safety for Channel-based Programming (extended version)
Go是一种生产级静态类型的程序设计语言，其设计特点是显式的消息传递原语和轻量级线程，使（并鼓励）程序员能够开发并发系统，其中组件通过通信进行交互，而不是基于锁的共享内存并发。Go语言只能在运行时检测全局死锁，但不能提供编译时保护来防止所有常见的通信不匹配或部分死锁。这项工作开发了一个静态验证框架，在Go程序的活性和安全性，能够检测通信错误和部分死锁在一般类的现实并发程序，包括那些与动态通道创建，无限线程创建和递归。我们的方法从Go程序中推断出其通信模式作为行为类型的忠实表示。通过检查通道使用的语法限制，被称为围栏，我们确保程序是由许多不同的通信模式，可以重复无限多次。这个限制允许我们实现过程来检查类型中的活性和安全性，这反过来又近似于Go程序中的活性和安全性。我们已经在一个工具链中实现了类型推断、活性和安全检查，并在公开的Go程序中进行了测试。注：这是POPL 2017中发表的一篇论文的修订扩展版本，详情请参见第13页。
2017-02-28 cs.LO cs.PL
Inferring Empirical Sound Resource Bounds via Symbolic Execution and Linear Programming (Extended Version)
University of Innsbruck（因斯布鲁克大学）
本文提出一种结合动态符号执行与混合整数线性规划的混合方法，实现了函数式程序最坏情况资源消耗经验性上界的推导，相关原型工具CompAS已在Zenodo公开。
2026-08-13 cs.PL
Recurrence Extraction for Functional Programs through Call-by-Push-Value (Extended Version)
分析程序复杂性的主要方法是提取和求解一个递归，这个递归用输入的大小来表示程序的运行时间。我们开发了一种方法，自动提取这种递归高阶递归函数程序的语法。产生的递归程序是使用递归的按名称调用语言的程序，它根据输入的大小显式计算运行时间。为了以统一的方式实现这一点，同时涵盖按名称调用和按值调用评估策略，我们使用按推值调用（CBPV）作为中间语言。最后，我们使用域理论来开发一个指称成本语义的递归。
2019-11-11 cs.LO cs.PL
Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (extended version)
全称量词经常出现在程序验证器产生的证明义务中，例如，将未解释的函数公理化和表示数组的属性。基于SMT的验证者通常通过E-匹配来推理它们，这是一种SMT算法，需要语法匹配模式来指导量词实例化。设计好的匹配模式是一项挑战。特别是，如果证明所需的量词没有实例化，过度限制的模式可能会导致虚假的验证错误;它们也可能隐藏不一致的公理化所导致的不合理性。在本文中，我们提出了第一种技术，识别和帮助用户补救过度限制匹配模式的影响。我们设计了一种新的算法来合成完成证明所需的缺失触发项。工具开发人员可以使用这些信息来改进他们的匹配模式，防止类似的验证错误，或者修复检测到的不合理性。
2021-12-14 cs.PL
Type Checking Program Code using SHACL (Extended Version)
基于图的数据格式（如RDF）的一个优点是它们在表示数据方面非常灵活。为了避免运行时错误，处理高度灵活的数据表示的程序代码表现出的困难是，它必须始终包括最一般的情况下，属性可能是设置值或可能不可用。已经设计了对随机数据结构实施约束的随机约束语言（SHACL）。我们提出了我们的方法，类型检查使用SHACL（TyCuS），查询RDF数据图验证的SHACL形状图的类型检查代码。为此，我们从查询中获得SHACL形状，并将数据形状和查询形状作为类型集成到$λ$ -演算中。我们为TyCuS提供了正式的基础和类型安全的证明。程序员可以使用我们的方法来处理RDF数据，简化，类型检查代码不会遇到运行时错误（通常的例外情况是类型检查不能防止访问空列表）。
2019-07-01 cs.PL
Papaya: Global Typestate Analysis of Aliased Objects Extended Version
类型状态是面向对象编程中使用的状态机，用于指定和验证对象上方法调用的正确顺序。为了避免不一致的对象状态，类型状态强制线性类型化，这消除了--或者最多是限制了--别名。然而，别名是编程中的一个重要特性，如果我们希望在真实世界的软件系统中采用类型状态，那么现有的类型状态限制太多。在本文中，我们提出了一个面向对象的语言类型系统与typestate注释，它允许不受限制的别名，而不是以前的方法，它不需要线性约束。类型状态分析是全局的，它跟踪整个程序图中的对象，这确保了良好类型的程序符合并完成声明的协议。我们实现了我们的框架在Scala程序设计语言，并说明我们的方法使用一个运行的例子，显示类型状态和别名之间的相互作用。
2021-07-27 cs.PL
Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version)
Go是一种流行的并发程序设计语言，这要归功于它能够有效地结合并发和系统编程。在Go程序中，许多并发错误可能是由数据竞争和通信问题引起的。在本文中，我们开发了一种基于行为类型的理论来静态检测Go程序中的数据竞争和死锁。我们首先使用Go内存模型中定义的happens-before关系，在Go程序模型上指定锁安全性、活动性和数据竞争属性。我们表示这些属性的程序中的$μ$演算模型的类型，并验证它们使用类型级别的模型检查。然后，我们扩展了框架，以考虑Go的通道，并实现了一个静态验证工具，可以检测并发错误。据我们所知，这是Go语言的第一个此类静态验证框架，统一分析了由共享内存访问和异步消息传递通信混合引起的并发错误。
2021-11-18 cs.LO cs.PL
Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis (Extended Version)
虽然许多主流语言（如Java、Python和C#）越来越多地采用函数式API来简化编程并提高并行化/性能，但没有有效的技术可以用于使用这些API将现有的命令式代码自动转换为函数式变体。针对这一问题，本文提出了一种基于归纳程序合成的编译方法，以实现现有代码的现代化。我们的方法是基于这样的观察，即绝大多数的源/目标程序在此设置满足一个假设，我们称之为跟踪兼容性：不仅程序共享语法相同的低级别的表达式，但这些表达式也采取相同的值在相应的执行轨迹。我们的方法利用这一观察结果来设计一种新的神经指导合成算法，该算法（1）使用一种称为同源语法网络（CGN）的新型神经架构，（2）利用一种concolic执行形式来基于计算过程中出现的中间值修剪部分程序。我们已经在一个名为NGST 2的工具中实现了我们的方法，并使用它将命令式Java和Python代码转换为分别使用Stream和functools API的函数变体。我们的实验表明，NGST 2显着优于几个基线，我们提出的神经架构和修剪技术是实现良好的结果至关重要。
2022-03-18 cs.PL
World Age in Julia: Optimizing Method Dispatch in the Presence of Eval (Extended Version)
动态规划语言面临着语义和性能方面的挑战，例如eval，它可以将新代码注入到正在运行的程序中。Julia程序设计语言引入了世界时代的新概念，将优化的代码与eval最具破坏性的副作用之一隔离开来：对现有函数定义的更改。本文提供了第一个正式的语义世界时代的核心演算命名朱丽叶，并显示了世界时代如何使编译器优化，如内联，在eval的存在。虽然Julia也为程序员提供了绕过world age的方法，但我们发现这种机制并没有被广泛使用：对4,000多个注册Julia软件包的静态分析显示，只有4-9%的软件包绕过了world age。这表明Julia的语义符合程序员的期望。
2020-10-16 cs.PL
Closing the Gap -- Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic -- Extended Version --
动态类型的面向对象语言使程序员能够编写优雅的、可重用的和可扩展的程序。然而，在当前的程序验证方法中，静态类型信息的缺失造成了显著的开销。我们的建议有两个方面：首先，我们提出了一个抽象层隐藏的复杂性动态类型时，提供了足够的类型信息。由于这本质上造成了验证静态类型程序的错觉，因此所需的工作量与静态类型的情况相当。其次，我们展示了如何所需的类型信息可以有效地获得所有类型安全的程序集成到霍尔逻辑的类型推断算法，产生一个半自动的过程，让用户专注于那些真正需要他的注意力的打字问题。虽然应用类型推断的动态类型的程序是一个行之有效的方法，现在，我们的方法补充了传统的软类型系统，除了修改程序（静态类型）和接受存在的运行时类型错误（动态类型）提供正式的证明作为第三种选择。
2015-01-12 cs.LO cs.PL cs.SE
Data Petri Nets meet Probabilistic Programming (Extended version)
German Research Center for Artificial Intelligence (DFKI)（德国人工智能研究中心）；University of Trier（特里尔大学）；Technical University of Denmark（丹麦技术大学）
本文提出将数据Petri网系统转换为多数概率编程系统支持的PP语言模型的方法，证明其可靠性与统计仿真保证，探讨了其在流程挖掘等场景的应用并实现了原型。
2024-06-12 cs.AI cs.PL
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)
近年来，随着操作语义和相关逻辑的发展，C11程序的演绎验证技术有了很大的进步。然而，这些语义和逻辑是在受限的环境中开发的，以避免稀薄空气读取问题。在本文中，我们提出了一个操作语义，利用线程内的偏序（称为语义依赖）诱导最近开发的指称事件结构为基础的语义。我们证明了我们的操作语义是健全的和完整的指称语义。我们提出了一个相关的逻辑，概括了最近Owicki-Gries框架RC 11（修复C11），并证明了使用这种逻辑的几个例子证明。
2021-08-03 cs.LO cs.PL
Type-Directed Discretization of Probabilistic Programs (Extended Version)
Cornell University（康奈尔大学）；ETH Zurich（苏黎世联邦理工学院）；University of Munster（明斯特大学）
该研究针对含连续分布的递归高阶概率程序，提出名为Slice的类型导向离散化变换，可将连续程序转化为离散形式以适配离散推理引擎，能处理现有系统无法应对的复杂连续程序且性能具竞争力。
2026-08-18 cs.PL
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -- Extended Version
在程序合成中，在简洁和强大的规范之间有一个众所周知的权衡：如果一个规范太冗长，它可能比程序更难写;如果它太弱，合成的程序可能不符合用户的意图。在这项工作中，我们探讨使用注释限制内存访问权限的程序合成，并表明，他们可以使规范更强大，同时保持令人惊讶的简洁。具体来说，我们增强了合成分离逻辑（SSL），一个框架，用于合成堆操作程序，只读借用的逻辑机制。我们观察到，这种简约和保守的SSL扩展在几个方面有利于合成，使其更具（a）表达性（以适度的注释开销实现更强的正确性保证），（b）有效（它产生更简洁和更易于阅读的程序），（c）高效（更快的合成），（d）鲁棒性（合成效率受搜索启发式选择的影响较小）。我们解释的直觉，并提供正式的治疗只读借用。我们证实了索赔（a）-（d）通过描述我们的量化评估的一系列标准的基准规格的各种堆操纵程序的感知合成实现。
2020-01-29 cs.LO cs.PL
Structuring the Synthesis of Heap-Manipulating Programs - Extended Version
本文描述了一种从分离逻辑中表达的声明性规范中综合带有指针的命令式程序的演绎方法。我们的合成算法作为输入的一对断言-一个前和一个后置条件-这描述了两个状态的符号堆，并得出一个程序，将一个状态转换为其他，由堆的形状指导。程序合成算法依赖于综合分离逻辑（SSL）的新框架，SSL概括了堆蕴涵$\mathcal{P} \vdash \mathcal{Q}$的经典概念，以将满足断言$\mathcal{P}$的堆转换为满足断言$\mathcal{Q}$的堆的可能性。合成程序表示转换蕴涵语句$\mathcal{P} \leadsto \mathcal{Q}$的证明项，并且合成过程对应于证明搜索。因此，衍生程序的正确建设，在这个意义上说，他们满足归因的前/后条件，并伴随着完整的证明推导，这可以独立检查。我们已经实现了一个证明搜索引擎的SSL形式的程序合成器称为SuSLik。为了提高效率，引擎利用SSL规则的属性，例如规则应用程序在单独堆上的可逆性和可交换性，来修剪它必须考虑的派生空间。我们解释和展示SSL的使用特征的例子，描述的SuSLik的设计，并报告我们的经验，使用它来合成一系列的基准程序操纵基于堆的链接数据结构。
2018-11-09 cs.PL
Refinement Kinds: Type-safe Programming with Practical Type-level Computation (Extended Version)
这项工作介绍了新的概念，细化，我们开发的上下文中明确多态ML类语言与类型级计算。正如类型精化通过类型域中的值上的谓词所表达的理解原则来嵌入丰富的规范一样，种类精化通过种类域中的类型上的谓词来提供丰富的种类规范。通过利用我们强大的细化类规则，我们语言中的类型不仅用于静态地对程序表达式和值进行分类，而且还可以方便地作为树状数据结构进行操作，并通过对此类结构的逻辑约束来细化它们的类。值得注意的是，由此产生的类型和分类规则允许强大的类型反射，ad-hoc多态和类型元编程，这些通常在现代软件开发中发现，但通常不能在通用语言中以类型安全的方式表达。我们通过建立类型安全的标准元理论结果，并通过一个原型实现的一种检查器，类型检查器和解释器，我们的语言，验证我们的方法在形式上和实用。
2019-08-01 cs.PL
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
提出Coneris，首个高阶并发分离逻辑，通过随机逻辑原子性支持并发概率程序的错误概率界模块化推理，并在Rocq和Iris中机械化验证。
2025-08-07 cs.LO cs.PL
An Incremental Slicing Method for Functional Programs
切片的几个应用程序需要一个程序相对于一个以上的切片标准进行切片。程序专门化、并行化和内聚性测量是这些应用的例子。这些应用程序可以受益于增量静态切片方法，其中相对于一个标准的切片计算的很大程度上可以重新用于另一个标准。在本文中，我们考虑的问题，增量切片的功能性程序。首先，我们提出了一个非增量版本的切片算法，它做一个多变量分析1的功能。由于多变量分析往往是昂贵的，我们计算每个函数的紧凑上下文无关的摘要，然后在函数的调用站点使用此摘要。函数摘要的构造非常重要，有助于增量版本的开发。另一方面，增量方法由一次性的预计算步骤组成，该步骤使用非增量版本相对于固定的默认切片标准对程序进行切片，并将结果进一步处理为规范形式。提出了一个实际的切片标准，增量步骤涉及一个低成本的计算，使用的结果，预先计算，以获得切片。我们已经实现了一个原型的切片器的一个纯子集的计划，对和列表作为唯一的代数数据类型。我们的实验表明，切片器的增量步骤比非增量版本快几个数量级。我们还证明了我们的增量算法的正确性，相对于非增量版本。
2017-09-23 cs.PL
Polyvariant Program Specialisation with Property-based Abstraction
在本文中，我们表明，基于属性的抽象，一个既定的技术起源于软件模型检验，是一个灵活的方法，在标准的在线专业化算法控制程序专业化的多变量。专业化是一种程序转换，它根据限制其行为的给定约束来转换程序。多变量专业化是指生成同一程序代码的两个或多个专业化版本。在计算过程中，同一个程序点可以不止一次地达到，每种情况下都有不同的约束条件，而多变量专业化允许实现不同的专业化。基于属性的抽象使用属性的有限集合来定义谓词的抽象版本的有限集合，确保仅生成有限数量的专用版本。属性的特定选择对于多元性至关重要;太少的版本可能导致专业化不足，而太多的版本可能导致代码大小的增加，而没有相应的效率增益。使用实例，我们展示了基于属性的抽象专业化的灵活性，并讨论了其在控制流细化，验证，终止分析和基于维度的专业化。
2019-08-20 cs.LO cs.PL
Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions (Extended Version)
在算法复杂性攻击中，恶意方利用算法的最坏情况行为来造成拒绝服务。一个突出的算法复杂性攻击是正则表达式拒绝服务（ReDoS），其中攻击者通过提供精心制作的输入字符串来触发匹配算法的最坏情况行为，从而利用易受攻击的正则表达式。本文提出了一种自动发现程序中的ReDoS漏洞的技术。具体来说，我们的方法自动识别程序中易受攻击的正则表达式，并确定是否可以将“邪恶”的输入字符串与易受攻击的正则表达式进行匹配。我们已经在一个名为REXPLOITER的工具中实现了我们提出的方法，并在Java Web应用程序中发现了41个可利用的安全漏洞。
2017-01-15 cs.CR cs.FL cs.PL
Complete Local Reasoning About Parameterized Programs Over Topologies (Extended Version)
University of Toronto（多伦多大学）
本文研究了无限状态参数化并发程序在丰富通信拓扑上的算法安全验证问题，提出通过全局量化归纳不变量自动证明正确性的方法，并通过多个拓扑的基准测试验证了该方法的有效性。
2026-07-22 cs.LO cs.PL
REST: Integrating Term Rewriting with Program Verification (Extended Version)
我们介绍REST，一种新的术语重写技术的定理证明，使用在线终止检查，并可以与现有的程序验证。REST通过以下方式为定理证明实现灵活但终止的项重写：（1）利用比标准重写简化排序更宽松的新引入的项排序;（2）基于迄今为止采取的重写路径动态和迭代地选择排序;以及（3）集成允许无法用重写规则证明的步骤的外部预言机。我们的REST方法是围绕一个易于实现的核心算法设计的，可以通过选择术语排序及其实现来参数化;通过这种方式，我们的方法可以很容易地集成到现有的工具中。我们将REST实现为Haskell库，并将其纳入Liquid Haskell的评估策略，通过重写规则扩展Liquid Haskell。我们通过将其与现有的重写技术和E-匹配进行比较来评估我们的REST实现，并表明它可以用于取代许多现有Liquid Haskell证明中的手动引理应用程序。
2022-02-17 cs.PL
Formally Validating a Practical Verification Condition Generator (extended version)
一个程序验证器产生可靠的结果，只有当两个逻辑用于证明程序的正确性是健全的，程序验证器的实现本身是正确的。尽管形式上证明逻辑的可靠性是很常见的，但验证器的实现通常仍然未经验证。验证器实现中的错误可能会危及成功验证结果的可信度。由于程序验证器在实践中使用的是复杂的，不断发展的软件系统，它通常是不可行的，正式验证其实现。在本文中，我们提出了一种替代方法：我们验证成功运行的广泛使用的布吉验证器通过产生一个证书，证明所获得的验证结果的正确性。Boogie执行一系列复杂的程序翻译，然后最终生成一个验证条件，其有效性应该意味着输入程序的正确性。我们将展示如何证明三个布吉的核心转型阶段：消除循环控制流路径，（SSA样）的假设使用新的变量（被动化），并最终生成的验证条件的替代分配。类似的翻译被其他验证者采用。我们的实现在Isabelle中生成证书，基于Boogie语言的新颖形式化。
2021-05-29 cs.PL
A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)
RWTH Aachen University（亚琛工业大学）；Saarland University（萨尔兰州立大学）；University College London（伦敦大学学院）；Technical University of Denmark（丹麦技术大学）
本文提出一个面向离散概率程序的定量验证基础设施，类似Boogie，采用实值逻辑和中间验证语言，支持期望性质验证，并基于SMT实现自动验证多种基准。
2026-09-24 cs.PL
GOOL: A Generic Object-Oriented Language (extended version)
我们提出了GOOL，一个通用的面向对象的语言。它证明了一种具有正确抽象的语言可以捕获面向对象程序的本质。我们展示了如何GOOL程序可以用来生成人类可读的，文档化的和惯用的多种语言的源代码。此外，在GOOL中，可以表达常见的编程习惯和模式，从简单的库级函数，到简单的任务（命令行参数，列表处理，打印），再到更复杂的模式，例如具有输入，输出和输入输出参数的方法，最后是设计模式（例如观察者，状态和策略）。GOOL是Haskell中的嵌入式DSL，可以生成Python，Java，C#和C++代码。
2019-11-26 cs.PL
An Abstract Domain for Heap Commutativity (Extended Version)
本文提出一种面向堆操作程序的抽象域，将具体堆程序的交换性验证转移到抽象数学模型上安全执行，并支持框架化与组合推理，已在 Coq 中完成机械化。
2024-11-25 cs.LO cs.PL
Achieving High Coverage for Floating-point Code via Unconstrained Programming (Extended Version)
实现高代码覆盖率在测试中至关重要，这使我们对代码质量充满信心。测试浮点代码通常需要在处理浮点约束方面付出艰苦的努力，例如，象征性的处决本文将测试浮点代码的挑战转化为应用无约束编程的机会--在整个搜索空间上计算函数最小点的数学解决方案。我们的核心见解是从浮点程序中导出一个表示函数，其任何最小点都是一个测试输入，保证可以运行被测试程序的一个新分支。这种保证允许我们通过反复最小化表示函数来实现浮点程序的高覆盖率。我们已经在一个名为CoverMe的工具中实现了这种方法，并在Sun的C数学库上对其进行了广泛的评估。我们的评估结果表明，CoverMe平均在6.9秒内实现了90.8%的分支覆盖率，大大优于我们比较的工具：（1）随机测试，（2）AFL，Google发布的高度优化，强大的模糊器，以及（3）Austin，一种最先进的基于覆盖率的测试工具，旨在支持浮点代码。
2017-04-11 cs.PL cs.SE
Optimistic Concurrency Control for Real-world Go Programs (Extended Version with Appendix)
我们提出了一个源到源的转换框架，GOCC，消费基于锁的悲观并发程序在Go语言，并将它们转换成乐观的并发程序，使用硬件transmittance内存（HTM）。选择Go语言的动机是并发性是Go语言中的一等公民，并且在Go程序中广泛使用。GOCC执行丰富的过程间程序分析，以检测和过滤锁保护区域，并在有利时执行周围锁的AST级代码转换。盈利能力由关键部分的静态分析和通过执行配置文件的动态分析驱动。一个自定义的HTM库，使用感知器，学习并发行为，并动态决定是否在重写的锁定/解锁点使用HTM。鉴于事务内存研究的丰富历史，但它缺乏在任何工业环境中的采用，我们相信这种工作流程，最终产生源代码补丁，更适合工业规模的采用。广泛采用的Go库和应用程序的结果表明，我们的自动化转换带来了显著的（高达10倍）和可扩展的性能提升，同时避免了重大的性能退化。
2021-06-03 cs.DC cs.PF cs.PL
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)
本文提出一种基于幽灵的并发程序正确性见证格式，使交错语义与线程模块化语义下的见证有效性一致，并在SV-COMP基准上验证了其可行性。
2024-11-25 cs.PL
Finite-Tree Analysis for Constraint Logic-Based Languages: The Complete Unabridged Version
基于有理树（可能是无限树）理论的逻辑语言有很大的吸引力，因为有理树允许更快的统一（由于安全地省略了发生检查）和增加的表达性（循环项可以提供语法和其他有用对象的非常有效的表示）。不幸的是，无限有理树的使用存在问题。例如，许多内置谓词和库谓词对于这样的树来说是不明确的，需要通过运行时检查来补充，其成本可能很高。此外，一些广泛使用的程序分析和操作技术只对那些在有限树上工作的程序部分是正确的。因此，重要的是自动获得程序变量（有限变量）的知识，在感兴趣的程序点处，这些变量将总是绑定到有限项。出于这些原因，我们在这里提出了一个新的数据流分析，基于抽象的解释，捕捉这样的信息。
2004-04-27 cs.PL
Products of Recursive Programs for Hypersafety Verification (Extended Version)
针对无限状态递归程序的自动超安全性验证问题，提出一类无限递归乘积程序，结合语言理论与并发理论构造算法，将超安全性验证简化为标准安全性验证，并通过实现和实验证明有效性。
2025-08-23 cs.LO cs.PL
Sound Static Deadlock Analysis for C/Pthreads (Extended Version)
提出了一种C/pthreads静态死锁分析方法。我们的方法的设计一直遵循的要求，分析现实世界的代码。我们的方法是合理的（即，对于那些根据C标准定义了行为的程序来说，它是没有死锁的），并且足够精确，可以证明大量程序的死锁自由。该方法由一个管道的几个分析，建立在一个新的上下文和线程敏感的抽象解释框架。我们进一步提出了一个轻量级的依赖分析，以确定相关的死锁分析，从而加快整体分析的语句。在我们的实验性评估中，我们在不到11小时的时间内成功地证明了Debian GNU/Linux发行版中262个程序的无死锁性，总共使用了2.6兆字节。
2016-07-23 cs.PL
Predicting All Data Race Pairs for a Specific Schedule (extended version)
我们考虑的问题，数据竞争预测程序的行为是由一个跟踪。跟踪是在程序执行期间记录的程序事件序列。我们采用可重复的发生之前的关系，以表征所有对的事件，在一个比赛中的时间表表现在跟踪。与经典的happens-before关系相比，可扩展的happens-before关系适当地处理了写-读依赖关系，从而避免了误报。挑战是有效地识别所有（可识别的）数据竞争对。我们提出了一个改进的线性时间向量时钟算法来预测许多可重复的数据竞争对。我们引入了二次时间后处理算法来预测所有剩余的数据竞争对。这提高了该领域的技术水平，我们的实验表明，我们的方法可以扩展到现实世界的例子。因此，用户可以系统地检查和修复在特定时间表的竞争中的所有节目位置。
2019-09-07 cs.PL
Program algebra for random access machine programs
本文提出了以随机存取机（RAM）指令为基本指令的指令序列的代数理论，讨论了指令序列在执行过程中所产生的行为，以及这些行为与RAM存储器之间的相互作用。该理论为诸如计算复杂性和算法分析等领域的理论发展提供了一种设置，该算法通过提供等式推理的可能性来确定指令序列是否计算给定函数而使其自身与众不同，并且比任何已知版本的RAM计算模型所提供的设置更通用。在此设置中，一个半现实的版本的RAM模型的计算和面向位的时间复杂度措施，这个版本的介绍。在所考虑的时间尺度下，半真实RAM可以用多带图灵机以二次时间开销来模拟。
2022-11-22 cs.CC cs.PL
Error Localization for Sequential Effect Systems (Extended Version)
本文提出一种基于有序代数结构残差概念的序列效应系统错误定位方法，保证在类型检查失败时提供与求值顺序相关的可预测错误位置，且报告位置显著更接近实际出错点。
2023-07-28 cs.PL
Verus: Verifying Rust Programs using Linear Ghost Types (extended version)
Rust程序设计语言提供了一个强大的类型系统，可以检查线性和借用，允许代码安全地操作内存而无需垃圾回收，使Rust成为开发低级别，高保证系统的理想选择。对于这样的系统，形式化验证可以用来证明类型安全之外的功能正确性。本文介绍了Verus，一个基于SMT的正式验证Rust程序的工具。通过Verus，程序员可以使用Rust语言表达证明和规范，允许证明利用Rust的线性类型和借用检查。我们展示了如何证明操作线性类型的权限，让Rust代码安全地操作内存，指针和并发资源。Verus使用一种新颖的模式系统来组织证明和规范，该模式系统将未检查线性和借用的规范与检查线性和借用的可执行代码和证明区分开来。我们形式化Verus的线性，借用，和模式在一个小的λ演算，我们证明类型安全和终止的规格和证明。我们展示了一系列的例子，包括指针操作代码（一个基于XOR的双向链表），代码内部可变性，并发代码Verus。
2023-03-11 cs.LO cs.PL
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
我们提出了一种新的方法来进行差异成本分析，给出了一个程序的修订，试图静态约束的差异，在两个程序版本之间的资源使用，或成本。差异成本分析特别有趣，因为它有许多引人注目的应用，例如在代码审查时检测资源使用回归或证明不存在某些侧通道漏洞。差异成本分析的一种现有方法是应用关系推理，该关系推理在概念上构造产品程序，在该产品程序上可以过度近似两个程序版本之间的成本差异。然而，任何关系方法中的一个重大挑战是有效地对齐程序版本以获得精确的结果。在本文中，我们的主要观点是，我们可以避免的需要和程序对齐的限制，如果相反，我们绑定的差异，而不是直接绑定的具体成本差异的两个成本约束摘要。特别是，我们的方法计算两个程序版本之间的成本的最大差异的阈值，同时使用两种成本约束摘要-一个潜在的功能，评估的上限为第一个程序中产生的成本和反潜在的功能，评估的下限为第二个程序中产生的成本。我们的方法有一些理想的属性：它可以是完全自动化的，它允许优化相对成本的阈值，它是适合的程序，是不是语法相似，它支持非确定性。我们已经评估了我们的方法的实施，从文献中收集的一些程序对，我们发现，我们的方法计算在大多数例子中的相对成本紧阈值。
2022-04-07 cs.PL
Reference Capabilities for Flexible Memory Management: Extended Version
本文提出基于引用能力的类型系统，实现Verona语言中区域隔离与灵活内存管理，支持对象在区域间移动，确保线程安全且开销可控。
2023-09-06 cs.PL
