Concolic Testing Heap-Manipulating Programs
Concolic测试是一种集随机测试生成和符号执行于一体的测试生成技术。现有的concolic测试引擎集中于数值程序。堆操作程序广泛使用复杂的堆对象，如树和列表。由于多种原因，测试这些程序具有挑战性。首先，这类程序的测试输入必须满足非平凡的约束条件，这些约束条件必须精确地指定。其次，在这样的程序中精确地编码和求解路径条件是具有挑战性的，并且通常是昂贵的。在这项工作中，我们提出了第一个concolic测试引擎称为CSF堆操作程序的基础上分离逻辑。CSF有效地结合了基于规格说明的测试和concolic执行的测试输入生成。它是一组具有挑战性的堆操作程序进行评估。结果表明，CSF生成有效的测试输入和高覆盖率。此外，我们表明，CSF可以潜在地用于与前提推理工具相结合，以减少用户的努力。
2019-07-12 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
Liveness-Driven Random Program Generation
随机生成的程序在测试编译器和程序分析工具中很受欢迎，通过随机测试发现了真实C编译器中的数百个错误。然而，现有的随机程序生成器可能会生成大量的死代码（其结果永远不会被使用的计算）。这使得相对较少的代码可以执行目标编译器的更复杂的优化。为了解决这个缺点，我们引入了活性驱动的随机程序生成。在这种方法中，随机程序是自底向上构造的，由同步结构数据流分析指导，以确保生成器永远不会生成死代码。该算法被实现为一个插件的框架框架。我们评估它相比，Csmith，标准的随机C程序生成器。我们的工具生成的程序可以编译成具有更复杂指令组合的更多机器码。
2017-09-13 cs.PL
Verifying Liveness Properties of ML Programs
高阶递归模式是布尔程序的高阶模拟;它们形成了函数程序的自然抽象类。我们提出了一个新的，有效的算法来检查由高阶递归方案生成的树的CTL性质，这是Kobayashi的基于交集类型的模型检验技术的扩展。我们表明，该算法的实现，THORS，执行良好的一些小的例子，我们演示了它如何可以用来验证OCaml程序的活性属性。示例属性包括诸如“所有打开的套接字最终都将关闭”和“锁将保持到文件关闭”之类的语句。
2020-12-24 cs.PL
Towards Patterns for Heaps and Imperative Lambdas
在函数式程序设计中，无点关系演算在程序构造的一般理论中已经取得了丰硕的成果，但对于特定的应用程序，逐点表达式可以更方便和更容易理解。在命令式编程中，精化演算已经被绑定到状态变量的逐点表达式，除了无处不在但不可见的堆。为了将点态与无点态结合起来，de Moor和Gibbons扩展了λ演算，并使用关系解释了非单射模式匹配。本文给出了该语言的一种语义，使用偏序之间的“理想关系”，以及使用谓词Transformers的第二种语义。第二种语义的动机是它与分离代数的潜在用途，用于作用于堆的程序中的模式匹配。在这些模型中，包括松弛贝塔和埃塔法律证明，并提出了一些开放的问题。
2015-10-19 cs.PL
Does Task Complexity Moderate the Benefits of Liveness? A Controlled Experiment
本研究针对实时编程特性益处缺乏明确实证的问题，通过37人对照实验探究任务复杂度对实时内省工具调试效率的调节作用，发现工具可显著缩短调试时间，但未证实任务复杂度的调节效应，为相关研究与环境设计提供参考。
2024-12-09 cs.PL
Heap vs. Stack: Analyzing Memory Allocations in C and C++ Open Source Software
该研究针对C和C++开源项目的内存分配展开，通过测试23个项目的797个用例，发现堆分配占比差异大且C++用堆频率低于C，打破了程序员会主动规避堆分配的假设。
2024-10-08 cs.PL
Diamonds are not forever: Liveness in reactive programming with guarded recursion
当设计函数式反应式编程（FRP）的语言时，主要的挑战是为用户提供一个简单、灵活的界面，以便在高抽象级别上编写程序，同时确保所有程序都可以用低级语言有效地实现。为了迎接这一挑战，一个新的家庭的模态FRP语言已被提出，在中野的守护不动点算子的变种用于编写递归程序，保证属性，如因果关系和生产力。作为一个明显的扩展，也有人建议使用线性时态逻辑（LTL）作为一种通过Curry-Howard同构进行反应式编程的语言，允许将终止，活性和公平性等属性编码在类型中。然而，这两个想法是相互冲突的，因为不动点算子将非终止性引入到应该提供终止保证的归纳类型中。在本文中，我们表明，关于模态时间步长运营商的LTL的一个子模态的一个用于保护递归（而不是等同于他们），可以得到一个模态类型系统能够表达活性性质，同时保留权力的保护不动点运营商。我们介绍的语言活泼的RaTT，一个模态FRP语言与守卫不动点运算符和一个“直到”类型的构造函数在LTL，并显示如何编程的事件和公平的流。使用一个步骤索引的Kripke逻辑关系，我们证明了活泼的RaTT的业务性质，包括生产力和因果关系，以及终止和活性预期的LTL类型的属性。最后，我们证明了Lively RaTT的类型系统保证了不存在隐式空间泄漏。
2020-08-20 cs.PL
Abstracting Runtime Heaps for Program Understanding
现代编程环境提供了广泛的支持，检查，分析和测试程序的基础上的算法结构的程序。不幸的是，对在执行期间检查和理解运行时数据结构的支持通常受到更多限制。本文提供了一种通用的技术来抽象和总结整个运行时堆。我们描述了抽象堆模型和相关的算法，用于将具体堆转储转换为相应的抽象模型，以及用于合并，比较和计算抽象模型之间的变化的算法。抽象模型旨在强调有关基于堆的数据结构的高级概念，如形状和大小，以及堆结构之间的关系，如共享和连接。我们通过构建一个内存分析器来展示抽象堆模型的实用性和计算易处理性。然后，我们使用这个工具来检查，查明和纠正来自DaCapo的一套程序的内存膨胀的来源。
2012-01-06 cs.PL cs.SE
Proving Liveness of Parameterized Programs
多线程程序的正确性通常要求它们满足活性属性。例如，程序可能要求没有线程缺少共享资源，或者所有线程最终都同意一个值。本文提出了一种方法来证明这样的活性性质举行。在这项工作中解决的两个特殊挑战是：（1）正确性论证可能依赖于系统的全局行为（例如，正确性论证可以要求所有线程共同地朝着“好的事情”前进，而不是一个线程前进而其它线程不干扰），以及（2）这样的程序通常被设计成由任何数量的线程执行，并且所期望的活跃度属性必须保持，而不管程序中活动的线程的数量如何。
2016-05-08 cs.LO 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
Arithmetizing Shape Analysis
针对链式堆数据结构程序的内存安全验证难题，提出结合流抽象与视图抽象的归约方法，将内存安全证明转化为无堆程序证明，可借助现成工具验证多种链式结构的顺序及并发程序的内存安全性。
2024-08-16 cs.PL
Espresso: Brewing Java For More Non-Volatility with Non-volatile Memory
快速、字节可寻址的非易失性存储器（NVM）包含接近DRAM的延迟和类似于盘的持久性，这已经产生了相当大的兴趣来革命性地改变系统软件栈和编程模型。然而，不太了解NVM如何与Java虚拟机（JVM）等托管运行时相结合，以简化持久性管理。本文提出了Espresso，一个整体的扩展，Java和它的运行时，使Java程序员利用NVM的持久性管理与高性能。Espresso首先提供了一个通用的持久化堆设计，称为Persistent Java Heap（PJH），用于将持久化数据作为普通Java对象进行管理。然后使用可恢复机制来加强堆，以提供堆元数据的崩溃一致性。然后，它提供了一个称为持久Java对象（PersistentJavaObject，PJO）的新抽象，为程序员持久化应用程序数据提供了一个易于使用但安全的持久编程模型。评估证实，Espresso显著优于最先进的NVM对Java的支持（即，JPA和PCJ），同时与Java程序中现有的数据结构兼容。
2017-10-27 cs.PL
Interacting via the Heap in the Presence of Recursion
几乎所有现代命令式程序设计语言都包含动态操作堆的操作，例如通过分配和释放对象，以及通过更新引用字段。在递归过程和局部变量的存在下，程序与堆的交互可能变得相当复杂，因为可以使用局部变量在调用堆栈上分配无限数量的对象，或者匿名地使用引用字段在堆上分配对象。因此，一般来说，静态分析是不可判定的。在本文中，我们研究了验证的递归程序与无界分配的对象，在一个简单的命令式语言堆操作。我们提出了一种改进的语义，这种语言，使用的抽象是精确的。对于任何具有有界可见堆的程序，这意味着在任何执行点从变量可到达的对象数量是有界的，这种抽象是其行为的有限表示，即使在状态中可能出现无限数量的对象。因此，对于这样的程序，模型检验是可判定的。最后，我们介绍了一个规约语言的时间属性的堆，并讨论了模型检验这些属性对堆操作程序。
2012-12-17 cs.LO cs.PL
Exploratory and Live, Programming and Coding: A Literature Study Comparing Perspectives on Liveness
各种编程工具，语言和环境给程序员的印象是在程序运行时更改程序。这种活跃的体验已经讨论了二十多年，关于这个主题的研究范围很广。除此之外，这项工作已经在社区中围绕三个主要的想法进行，其中包括活跃性作为一个重要方面：实时编程，探索性编程和实时编码。虽然有关于每个特定社区的重点的出版物，但这三个社区的整体活跃度尚未调查。因此，我们想描绘各种研究的活性。与此同时，我们希望调查这三个社区在价值观和贡献方面的重叠和差异。因此，我们进行了一项文献研究的样本212出版物的检索词从三个主要的索引服务。在这个样本上，我们进行了主题分析，涉及以下方面：活跃的动机，应用领域，运行系统的预期结果，以及贡献的类型。我们还收集了相关关键词和著名出版物等书目信息。研究结果表明，探索性程序设计的领域主要是通用程序设计工具的技术设计和实证研究。相比之下，关于实时编码的出版物在动机和方法上最多样化，其中大多数是对用户的实证研究。正如预期的那样，大多数关于现场编码的出版物都应用于行为艺术。最后，关于现场编程的研究主要是为了使编程更容易获得和更容易理解，通过与用户的实证研究来评估他们的工具设计。在描绘关于活力的工作范围时，我们希望使各个社区更加了解其他社区的工作。此外，通过概述各个社区的价值观和方法，我们希望为活跃度领域的新研究人员提供初步的概述。
2018-07-23 cs.PL cs.SE
Liveness for Verification
我们探讨使用活性的交互式程序验证一个简单的并发对象语言。我们的实验IDE集成了两种（正式双）持续测试到开发环境中：兼容性检查，它验证一个对象的使用其他对象，和合规性检查，它验证一个对象的要求，以完善另一个对象的行为。IDE突出显示的源代码错误不是静态类型错误，而是在系统的某些执行过程中发生的运行时错误的源代码反射。我们展示我们的方法，并讨论机遇和挑战。
2016-09-14 cs.PL
SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic
我们引入了一种新的动态分析技术来发现堆操作程序的分离逻辑中的不变量。首先，我们使用一个调试器，以获得丰富的程序执行跟踪在感兴趣的位置上的样本输入。这些跟踪由指向动态分配的数据结构的变量的堆和堆栈信息组成。接下来，我们迭代地分析与每个指针变量相关的单独的内存区域，并在分离逻辑中的预定义堆谓词上搜索公式来对这些区域进行建模。最后，我们将计算公式组合成一个不变的描述探索的记忆区域的形状。我们提出了SLING，一个实现这些思想的工具，可以在C程序的任意位置自动生成分离逻辑中的不变量，例如，程序前置和后置条件以及循环不变式。现有基准测试的初步结果表明，SLING可以有效地产生正确的和有用的不变量的程序，操纵各种复杂的数据结构。
2019-06-29 cs.PL
An Abstract Domain for Heap Commutativity (Extended Version)
本文提出一种面向堆操作程序的抽象域，将具体堆程序的交换性验证转移到抽象数学模型上安全执行，并支持框架化与组合推理，已在 Coq 中完成机械化。
2024-11-25 cs.LO cs.PL
Program Optimization Based Pointer Analysis and Live Stack-Heap Analysis
在本文中，我们提出了类型系统的流敏感指针分析，活堆栈堆（变量）分析和程序优化。用于活堆栈-堆分析的类型系统是指针分析的类型系统的丰富;该丰富具有添加到后一系统的类型的第二组件的形式。指针分析的结果被证明是有用的，通过使用它们在类型系统的活堆栈堆分析。用于程序优化的类型系统也是用于活堆栈-堆分析的类型系统的扩充，但是扩充采取了将转换组件添加到后一系统的推理规则的形式。实现程序优化的形式是死代码消除。一种形式的程序纠正可能间接地导致消除错误的代码（导致程序中止），这是死的。因此，程序优化可以导致程序校正。我们的类型系统具有组合和相对简单结构的优势。我们的工作的新颖性来自于这样一个事实，即我们的类型系统的程序优化相关联的优化版本的程序的理由（在类型派生的形式）的优化。这个理由在许多研究领域都非常受欢迎，比如认证代码（证明携带代码），这是这项工作的动机
2011-04-04 cs.PL cs.SE
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
Spencer: Interactive Heap Analysis for the Masses
程序设计语言-设计和运行时-实现需要关于用户想要实现的程序的详细知识。获取这些知识是困难的，并且几乎没有工具支持来有效地估计所提出的权衡在现实世界应用程序的上下文中是否实际上有意义。理想情况下，关于“典型”程序行为的知识是1）容易获得的，2）容易复制的，以及3）容易共享的。我们提出了斯宾塞，一个Web服务和API框架的动态分析的一组不断增长的标准程序语料库的痕迹。用户不能自己获取跟踪，而是可以向Web服务发送查询，这些查询将在一组程序跟踪上执行。查询组合符是一组查询组合符的内置的项，它们提供了一个用于处理跟踪数据的高级接口。由于框架是高级的，并且有一个托管的记录跟踪集合，因此查询很容易实现。由于数据集由研究界共享，因此结果是可重复的。由于实际的查询运行在一个（或多个）提供分析服务的服务器上，因此可以在商用硬件上获得结果。Spencer中的数据意味着只获取一次，并经常进行分析，这使得数据汇集的开销几乎无关紧要。这使得Spencer能够收集比传统跟踪工具在其性能预算范围内所能提供的更多的数据。Spencer中的结果被缓存，使得基于缓存的原语查询的复杂分析变得更快。
2017-03-31 cs.PL
Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
我们调查的可判定性的自动程序验证的程序，操作堆，特别是，决策程序证明内存安全。我们最近的工作，确定了一个可判定的子类未解释的程序，一类别名感知的程序，可以更新地图。我们应用这一理论来开发验证算法的内存安全-确定如果一个堆操作程序，分配和释放内存位置和操作堆指针不引用未分配的内存位置。我们表明，这个问题是可判定的，当初始分配的堆形成一个森林的数据结构，当程序流一致，直观地限制程序，使一个单一的数据结构通过。我们的一组库例程，操纵森林数据结构的实验评估表明，常见的单通算法的数据结构往往属于可判定类，我们的决策过程是有效的，在验证它们。
2019-12-31 cs.FL cs.LO cs.PL
Shape Neutral Analysis of Graph-based Data-structures
格式错误的数据结构可能导致运行时错误，如任意内存访问或损坏。尽管如此，低级别堆操作程序的数据结构属性推理仍然具有挑战性。在本文中，我们提出了一个基于约束的程序分析，检查数据结构的完整性，w.r.t.给定目标数据结构属性，因为堆由程序操纵。我们的方法是使用来自目标程序的类型定义自动生成属性的求解器。生成的求解器是使用内置堆、整数和等式求解器的约束处理规则（Constraint Handling Rules，简称CLR）扩展实现的。我们的程序分析的一个关键属性是目标数据结构属性是形状中性的，即，该分析不检查与给定数据结构图形形状相关的属性，例如双链表与树。尽管如此，分析可以检测到错误的数据结构操作程序，包括那些使用列表，树，DAG，图形等，我们提出了一个实现，使用的可满足性模约束处理规则（SMESTO）系统。实验结果表明，我们的方法可以很好地为现实世界的C程序。
2018-05-03 cs.PL
Distributed Data and Programs Slicing
本文提出了一种新的技术，数据切片的分布式程序上运行的层次结构的机器。数据切片可以实现为一种程序转换，将层次结构中的机器堆划分为独立的区域。在每台机器的每个区域内，指针保留原始堆层次结构中的原始指针结构。基本类型的每个堆组件（例如，整型）仅进入堆之一的区域。所提出的技术具有推理规则系统的形状。此外，本文还提出了一种结构简单的类型系统来判定分布式程序的类型可靠性。使用这种类型系统，数学证明，建议的切片技术保持类型属性概述了本文。
2014-02-24 cs.PL cs.SE
Predicate Abstraction for Linked Data Structures
本文提出了一种新的验证链接数据结构正确性的方法-虽然有许多技术可以检查堆操作程序是否符合其规范，但它们通常需要程序员注释每个过程的行为，例如，以循环不变式和前置条件和后置条件的形式。谓词抽象将是执行不变推理的一个有吸引力的抽象域，现有技术不能以足够的精度来推理堆以验证数据结构操纵程序的功能属性。在本文中，我们提出了一种技术，通过将数据结构的分析分解为两个正交分量，将谓词抽象提升到堆中：（1）优化类型，它推理堆结构的物理形状，以及（2）细化类型，它使用来自SMT可判定理论的简单谓词来捕获结构的逻辑或语义属性。我们通过将类型转换为分离逻辑断言来证明ART的可靠性，从而将ART中的类型推导转换为分离逻辑证明。我们评估艺术通过实现一个工具，执行类型推断的命令式语言，并凭经验表明，使用一套数据结构基准，艺术只需要21%的注释所需的其他国家的最先进的验证技术。
2015-10-31 cs.PL
FO-Complete Program Verification for Heap Logics
University of Wisconsin–Madison（威斯康星大学麦迪逊分校）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
本文提出两种堆逻辑，通过FO-完备性保证程序验证的正确性，并展示了其在数据结构验证中的有效性。
2026-01-10 cs.LO cs.PL
Debug-Localize-Repair: A Symbiotic Construction for Heap Manipulations
我们提出Wolverine 2，一个集成的堆操作程序的本地化修复环境。Wolverine 2提供了一个交互式的调试环境：当具体执行一个程序通过一个交互式的外壳上支持常见的调试设施，Wolverine 2显示抽象的程序状态（框和箭头图）作为一个视觉援助的程序员，包装一个新的，证明导向修复算法，快速合成修复补丁和一个新的错误定位算法，以减少搜索空间的修复。Wolverine 2支持生成的补丁的“热修补”，以提供无缝的调试环境，并且还促进了新的调试-本地化-修复可能性：\textit{specification refinement}和\textit{checkpoint-based hopping}。我们评估Wolverine 2上6400错误程序（使用自动故障注入生成）的各种数据结构，如单，双，循环链表，AVL树，红黑树，八字树和二叉搜索树; Wolverine 2可以修复所有的错误实例在现实的程序员等待时间（在大多数情况下小于5秒）。Wolverine 2还可以修复超过80%的247（错误）学生提交的合理尝试。
2022-02-02 cs.PL cs.SE
S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs
众所周知，堆操作程序是很难推理的。我们提出了一种新的验证器堆操作程序称为S2 TD，它编码的程序系统的形式约束角子句（CHC）使用一种新的扩展分离逻辑（SL）与递归谓词和悬空谓词。S2 TD积极探索循环证明来解决路径爆炸问题。S2 TD区别于现有的基于CHC的验证程序，专注于堆操作程序，并采用循环证明来有效地验证或证伪它们与反例。与现有的基于SL的验证器相比，S2 TD精确地指定了解除分配的指针堆，以避免错误存在的推理中的误报。S2 TD已经使用来自SV-COMP存储库的一组全面的基准程序进行了评估。结果表明，S2 TD比最先进的程序验证器更有效，比大多数程序验证器更高效。
2022-09-19 cs.PL cs.SE
Increasing the Expressiveness of a Gradual Verifier
本文通过为渐进式验证器 Gradual C0 扩展展开表达式支持，提升其规范语言的表达能力，从而实现对递归堆数据结构更直观的规范描述。
2025-07-17 cs.PL
A Modular Framework for Stack-Heap and Value Abstractions (Extended Version)
Ca’ Foscari University of Venice（威尼斯大学）
本文针对高级静态程序分析中不同编程语言内存管理问题，提出并形式化通用内存框架，基于抽象解释理论，通过分裂状态抽象将值与内存分析分离到模块化域，可支持多种语言行为，独立组合不同分析。
2026-07-20 cs.PL cs.SE
Live, Rich, and Composable: Qualities for Programming Beyond Static Text
推动编程超越静态文本代码的努力已经寻求向编程注入多种不同的品质。一个长期公认的特性是活跃性：在程序编辑时为程序员提供关于程序动态行为的深入反馈。第二个品质，长期探索但缺乏共同的艺术术语，是丰富性：允许程序员通过特定领域的表示和交互来编辑程序，而不仅仅是通过文本。在本文中，我们映射这两个品质之间的关系，并调查过去的工作，证明他们。我们观察到，结合了活性和丰富性的系统往往是以牺牲传统编程的一个基本品质为代价的：可组合性。我们认为，通过结合活性，丰富性和可组合性，编程系统可以更好地捕捉交互式计算的全部潜力，而不会留下传统代码的表现力。
2023-03-12 cs.HC cs.PL cs.SE
Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference (Extended Version)
在用于信息流控制的可靠的面向对象程序分析领域中，很少有方法采用堆的流敏感抽象来实现隐式流的精确建模。为了应对这一挑战，我们提出了一种新的符号抽象方法，用于在类Java程序中对堆进行建模。我们使用一个无存储的表示，参数化的家庭之间的关系的参考，提供不同程度的精度，根据用户的喜好。这使我们能够自动推断多态信息流警卫的方法，通过一个符号有限状态系统的可达性分析。我们用三个不同的关系族实例化堆抽象。我们证明了我们的方法的合理性，并通过使用IFSpec基准测试和现实生活中的应用程序与每个实例化堆域获得的精度和可扩展性进行比较。
2022-11-07 cs.CR cs.FL cs.PL
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
我们研究的多线程，共享内存程序，其中每个线程可以产生额外的线程的活性属性的上下文有界的验证。我们的主要结果表明，上下文有界的公平终止是可判定的模型，上下文有界意味着每个派生线程可以上下文切换一个固定的常数倍。我们的证明是技术性的，因为公平终止需要推理无限多线程的组成，每个线程都有无限大的堆栈。事实上，解决相关问题的技术，主要依赖于用有限状态线程替换下推线程，是不适用的。相反，我们引入一个扩展的矢量加法系统与状态（VASS），称为VASS气球（VASSB），作为一个中间模型，它是一个独立的兴趣无限状态模型。VASSB允许标记本身就是标记（气球）。我们表明，上下文有界的公平终止减少到公平终止VASSB。我们发现后一个问题是决定性的，显示了一系列的减少：从公平终止配置可达性VASSB，并从VASS的可达性问题。对于下限，在线程运行到完成（没有上下文切换）的特殊情况下，公平终止已经被认为是非基本的。我们还表明，更简单的问题，上下文有界终止是2 EXPSPACE-完整的，匹配的复杂性限制-和技术-安全验证。此外，我们还展示了公平饥饿的相关问题，它检查一些线程是否可以沿着公平运行饥饿，在上下文有界的情况下也是可判定的。可判定性采用了从公平饥饿到公平终止的复杂还原。和公平终止一样，这个问题也是非初等的。
2020-11-12 cs.FL cs.PL
Algorithmic Verification of Single-Pass List Processing Programs
我们引入了流数据串转换器，其在线性时间中以单次从左到右通过将输入数据串映射到输出数据串。数据字符串是数据值的（无界）序列，标记有有限集合中的符号，在一个潜在的无限数据域上，只支持相等和排序的操作。传感器使用有限的状态集、在数据域上的有限的变量集和在数据串上的有限的变量集。在每一步，它可以根据下一个输入符号做出决定，更新其状态，记住其数据变量中的输入数据值，并通过连接数据串变量和由数据变量形成的新符号来更新数据串变量，同时避免重复。我们建立的问题，检查两个流式传感器的功能等效性，并检查是否流传感器满足前/后验证条件流接收器指定的输入/输出数据串，在PSPACE。我们确定了一类命令和一类函数程序，操纵列表的数据项，可以有效地转换为流数据串换能器。命令式程序通过改变堆节点的下一个指针和添加新节点来动态修改单链堆。主要限制指定了下一个指针如何用于遍历。我们还确定了一个表达等效的函数程序片段，遍历一个列表使用语法限制递归调用。我们的研究结果导致算法的断言检查和检查功能等价的两个程序，写在不同的编程风格，常用的例程，如插入，删除，和反向。
2011-02-14 cs.PL
Spatial Interpolants
我们提出了分裂，一种新的技术证明堆操作程序的属性，婚姻（1）一个新的分离逻辑为基础的分析堆推理与（2）一个插值为基础的技术，用于精炼堆形状不变量与数据不变量。Splinter是属性导向的，精确的，当属性不成立时会产生反例跟踪。使用空间插值模理论的新概念，Splinter可以推断出一般递归谓词上的复杂不变量，例如，链表中的所有元素都是偶数或二叉树排序的形式。此外，我们将插值视为黑盒，这使我们能够自由地在任何合适的理论中为给定程序编码数据操作（例如，位向量、数组或线性算术），因此我们的技术立即受益于SMT求解和插值的任何未来进展。
2015-01-16 cs.LO cs.PL
A Logical Programming Language as an Instrument for Specifying and Verifying Dynamic Memory
这项工作提出了一个Prolog方言的表达性和自动化的发现和优先级的问题。给定某个类C程序，如果动态内存在运行时被分配、更改和释放，那么对所需动态内存的描述就是堆规范。根据给定规范检查计算的存储器状态是动态存储器验证。本文只考虑了Hoare演算中的形式规范和验证。发现的问题包括：无效分配、存储单元中的（临时）不可用数据、过多的存储器分配、意外区域中的（意外）堆更改等。过多的内存分配现在已经被像Valgrind这样的内存分析器成功地解决了。从本质上讲，这些领域的论文并没有带来任何大的突破。可能的原因还包括由于更多的可用内存和并行线程而导致的张力降低。然而，从Apt开始，与可变模式有关的问题尚未得到解决-既没有完全解决，也没有以可接受的方式解决。过去几十年的研究成果一次又一次地表明，堆问题仍然存在，仍然很复杂，仍然很重要。Peter O 'Hearn在2016年做出了重大贡献，他因其空间堆操作的并行方法而获得哥德尔奖。
2021-04-04 cs.FL cs.LO cs.PL
Unboxing Virgil ADTs for Fun and Profit
本文探索在系统级编程语言 Virgil 中通过 #unboxed 和 #packed 注解引导 ADT 表示优化，消除堆分配开销并支持自定义位布局，以节省内存并满足硬件数据格式要求。
2024-10-14 cs.PL
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
本文提出Trillium分离逻辑框架，通过内涵细化方法强化高阶并发与分布式分离逻辑，支持证明非平凡的安全性和活性属性，并分别实例化出Fairis和扩展Aneris以验证并发与分布式系统的活性及与TLA+模型的细化关系。
2024-08-22 cs.LO cs.PL
Object Graph Programming
本文提出对象图编程（OGO），通过声明式查询将对象堆视为图数据库，利用Cypher语言实现查询与修改，适用于集合查询、运行时内省和断言，并在Java中实现两种原型，验证于大型开源项目。
2024-02-04 cs.DB cs.PL cs.SE
General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
本文从语言理论角度研究异步共享内存程序，证明了高阶异步程序的安全、终止和有界性验证可判定，而二阶异步程序的活性验证不可判定，并揭示了判定性与底层语言类空性及“等字母”问题的联系，闭合了判定性边界。
2022-10-20 cs.FL cs.PL
Getting a Handle on Unmanaged Memory
本文提出编译器与运行时系统 ALASKA，通过句柄间接层使非托管语言中的堆对象可移动，从而以 malloc 直接替代品的方式实现压缩去碎片化，在 Redis 中降低内存使用达 40%。
2024-03-26 cs.OS cs.PL
Reversible Lifetime Semantics for Quantum Programs
Università di Catania（卡塔尼亚大学）；Université de Rouen Normandie（诺曼底鲁昂大学）
本文提出量子程序中可逆计算的语义基础，通过寿命引导的反向计算模型，定义了语义寿命和恢复不变量，证明了嵌套作用域下的组合正确性，并展示了早期回收如何减少电路深度和限制峰值活量子比特。
2026-03-15 cs.PL quant-ph
Verifying Temporal Properties of Reactive Systems by Transformation
我们展示了如何程序转换技术可以用于验证反应系统的安全性和活性特性。特别是，我们展示了如何程序转换技术蒸馏可以用来转换反应系统指定的功能语言成一个简化的形式，随后可以分析，以验证系统的时间属性。示例系统的目的是模型互斥分析使用这些技术的安全性（互斥）和活性（非饥饿），与错误，它们包含被正确识别。
2015-12-12 cs.LO cs.PL
Compositional Verification in Concurrent Separation Logic with Permissions Regions
本文提出带权限区域的 CSL-Perm 组合式验证系统，通过可推断框架规则残余堆的蕴涵过程实现线程与函数调用推理，并经 CoSl 工具验证其优势。
2025-10-06 cs.LO cs.PL
Effectiveness of Garbage Collection in MIT/GNU Scheme
Scheme使用垃圾回收进行堆存储管理。理想情况下，垃圾收集器应该能够回收所有死对象，即将来不会使用的对象。但是，垃圾收集器只收集那些无法从任何程序变量访问的死对象。可从程序变量访问的死对象不会被回收。在本文中，我们描述了我们的实验来衡量垃圾回收的有效性，在MIT/GNU计划。我们计算对象的拖动时间，即对象在最后一次使用后在堆内存中保留的时间。死亡对象的数量和拖动时间共同表明了改进垃圾回收的机会。我们的实验表明，多达26%的死亡对象仍然存在于内存中。平均拖动时间高达执行时间的37%。总体而言，我们观察到内存节省潜力从9%到65%不等。
2007-09-01 cs.PF cs.PL
CUP: Comprehensive User-Space Protection for C/C++
C/C++应用程序中的内存损坏漏洞使攻击者能够执行代码、更改数据和泄漏信息。当前的内存消毒器不提供程序数据的全面覆盖。特别是，现有的工具主要关注堆分配，对堆栈分配和全局变量的支持有限。此外，现有的工具专注于主要的可执行文件，对系统库的支持有限。此外，它们遭受假阳性和假阴性。我们提出了C/C++的全面用户空间保护CUP，这是一种LLVM消毒器，为64位架构上的C/C++程序提供完整的空间和概率临时内存安全（具有x86_64的原型实现）。CUP使用混合元数据方案，支持所有程序数据，包括全局变量、堆或堆栈，并维护ABI。与NIST Juliet测试套件的现有方法相比，CUP与最先进的LLVM消毒剂相比，将假阴性减少了10倍（0.1%），并且不会产生假阳性。CUP检测所有用户空间代码，包括libc和其他系统库，将它们从受信任的代码库中删除。
2017-04-17 cs.CR cs.PL
A novel datatype architecture support for programming languages
从程序员的角度来看，程序设计语言级的数据库具有简单的描述，而在硬件内部，庞大的机器码负责描述类型特征。数据类型架构设计是一种将编程特性与硬件设计相匹配的新方法。根据程序设计语言的重要数据类型（SDT），提出并实现了一种新的基于数据类型的代码缩减器（TYPELINE）结构。TYPELINE使用TEU处理各种SDT操作。这种结构设计减少了机器码的数量，提高了执行速度，同时也提高了一定的并行度。这是因为该体系结构支持并行执行抽象数据类型的某些操作。此外，它确保使用所提出的类型转换单元来维护数据类型特征和整个应用级规范。该框架包括编译器级执行模式识别和存储管理单元，通过ISA支持减少堆内存中对象的读写。这种节能架构与面向对象的程序设计语言完全兼容，并且在组合模式下，它可以处理关于并行TYPELINE架构支持的复杂C++数据结构。
2014-02-01 cs.PL
Test Case Generation for Object-Oriented Imperative Languages in CLP
测试是软件开发过程的重要组成部分。测试用例生成（Test Case Generation，TCG）是自动生成应用于被测系统的测试用例集的过程。白盒TCG通常通过符号执行来执行，即，代替对正常值执行程序（例如，numbers），则程序在表示任意值的符号值上执行。在处理面向对象（OO）命令式语言时，符号执行变得具有挑战性，因为它必须能够回溯，复杂的堆分配数据结构应该在TCG过程中创建，并且必须考虑继承，虚拟调用和异常等特性。由于其固有的符号执行机制，我们追求在本文中，约束逻辑程序设计（CLP）有一个很好的未开发的应用领域在TCG。我们将支持我们的主张，开发一个完全基于CLP的框架，以TCG的面向对象的命令式语言，并通过评估它对一组具有挑战性的Java程序的相应实现。我们的方法的一个独特的特点是，它只使用CLP来处理所有的语言特征，而不需要开发特定的约束运算符（例如，对堆进行建模）。
2010-07-29 cs.PL cs.SE
A Type-Based Complexity Analysis of Object Oriented Programs
介绍了一种面向对象的通用程序设计语言的类型系统，以推断资源上界。得到了多项式时间可计算函数集的一个可靠而完整的刻画。因此，类型化程序的堆空间和栈空间需求也是多项式有界的。这种类型系统的灵感来自于以前关于隐式计算复杂性的工作，使用分层和非干扰技术。所提出的方法有几个优点。首先，它为程序员提供了显式的大$O$多项式上界，因此它的使用可以允许程序员避免内存错误;其次，类型检查在多项式时间内是可判定的。最后，它具有良好的表达能力，因为它分析了大多数面向对象的特性，如继承，重载，重写和递归。此外，它可以处理由对象保护的循环，也可以扩展到改变控制流的语句，如break或return。
2018-02-19 cs.LO cs.PL
ShellVis: Sandboxed Live Programming for Shell Scripts
University of Washington（华盛顿大学）
ShellVis通过沙箱化文件系统实现Shell脚本的实时编程，提供逐行反馈，帮助用户安全调试并增强信心。
2026-09-11 cs.HC cs.PL
An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support
基于不变式的编程（IBP）是一种基于结构的正确的编程方法，其中程序是围绕不变式构建的，这些不变式在实际代码之前被另外制定。Socos是一个专门为支持IBP而构建的程序构建和验证环境。Socos的前端是一个图形化的图表编辑器，允许程序员构建基于不变式的程序并检查其正确性。Socos的后端组件，程序检查器，计算程序的验证条件，并试图自动证明它们。它使用定理证明器PVS和SMT求解器Yices来尽可能多地释放验证条件，而无需用户交互。在本文中，我们首先从用户和系统级的角度描述了Socos环境，然后通过在Socos中构建一个经过验证的堆排序实现来验证IBP工作流。案例研究突出了自动和交互式定理证明在IBP工作流程的三个连续阶段的作用：开发的背景理论，制定程序规范和不变量，并证明最终实现的正确性。
2012-02-22 cs.LO cs.PL
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
本文提出首个针对随机化伸展树等自调整数据结构的全自动化期望摊还成本分析方法，基于带类型与效应的系统并支持离散分布采样与计时算子，给出两个可靠性定理及原型实现。
2024-06-03 cs.DS cs.LO cs.PL
