JavaTA: A Logic-based Debugger for Java
本文提出了一种基于逻辑的Java程序调试方法。与传统的调试相比，我们提出了一种调试方法，Java程序使用逻辑查询的个人执行状态，也在历史上的执行。这些查询是通过我们早期研究中对面向对象程序错误的系统研究得出的。我们用一个逻辑数据库来表示Java程序执行过程中的显著事件，并将查询实现为逻辑程序。这种方法使我们能够回答一些有用的和有趣的查询有关的Java程序，如调用序列，在一定的结果，在一个特定的执行点的对象的状态等，我们的系统还提供了在调试会话期间组成新的查询的能力。我们相信，逻辑编程提供了一个面向对象的程序调试艺术的显着贡献。
2007-01-17 cs.PL
Remote Concolic Multiverse Debugging -- Extended Version with Additional Appendices
Ghent University（根特大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
本文提出基于跟踪的多宇宙调试器，结合符号执行与实时调试，有效减少状态空间并提升微控制器上非确定性程序调试的效率与可行性。
2026-04-28 cs.PL
Quantitative Analysis of Assertion Violations in Probabilistic Programs
在这项工作中，我们考虑的基本问题，得出定量界的概率，一个给定的断言违反概率程序。我们提供了自动化算法，以指数形式获得断言违规概率的下限和上限。我们的方法的主要新颖之处在于，我们证明了新的和专用的不动点定理，作为我们的算法的理论基础，使我们能够推理断言违反边界的前和后不动点函数。为了合成这样的不动点，我们设计的算法，利用广泛的数学工具，包括排斥排名超鞅，Hoeffding引理，闵可夫斯基分解，詹森不等式，凸优化。在理论方面，我们提供了（i）第一个自动算法的断言违反概率的下限，（ii）第一个完整的算法的仿射程序中的指数形式的上限，和（iii）可证明和显着更严格的上限比以前的方法的随机不变量。在实践方面，我们表明，我们的算法可以处理各种各样的方案，从文献和合成的界限，是几个数量级更紧，与以前的方法相比。
2020-12-01 cs.PL
Reversible Language Extensions and their Application in Debugging
有一系列的方法和技术可用于指导语言扩展和领域特定语言的设计和实现。一种简单而强大的技术是基于跨基本语言的编译通道交错的源到源转换。尽管是一种成功的方法，但它的主要缺点是输入源代码在过程中丢失。当考虑到程序开发的整个工作流程（警告和错误报告、调试，甚至程序分析）时，程序翻译并不比美化的宏语言更强大。在本文中，我们提出了一种增强的方法，语言扩展的Prolog，符号注释包括在目标程序。这些注释允许有选择地反转翻译的代码。我们说明了这种方法，通过显示，耦合它与最小的扩展到一个通用的Prolog调试器，使我们能够为用户提供一个熟悉的，源代码级的视图，在调试过程中使用的各种语言扩展，如功能符号，DCG，或CLP{Q，R}的程序。
2013-01-31 cs.PL
Visualizing the Evaluation of Functional Programs for Debugging
本文提出一种函数式程序可视化原型，通过解释抽象语法树与美化打印为OCaml生成求值可视化，探讨空间限制、非纯特性等挑战，旨在服务程序调试。
2024-11-01 cs.PL
Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
本文提出一种静态验证高阶（约束）逻辑编程程序中高阶断言的新方法，通过细化谓词属性语义并归约为一级属性，利用抽象解释实现编译时验证，并在Ciao系统中实现和评估。
2025-09-10 cs.PL
Reversible Debugging in Logic Programming
可逆调试在定位错误源方面变得越来越流行。这种技术提出了一种更自然的调试方法，其中可以从可观察到的错误行为向后探索计算错误的来源。在这项工作中，我们提出了一个可逆的调试方案的逻辑程序。为此，我们定义了一个适当的仪表化语义（所谓的Landauer嵌入），使SLD分辨率可逆。Prolog的一个可逆调试器的实现已经开发出来，并公开提供。
2022-06-20 cs.LO cs.PL
PolyDebug: A Framework for Polyglot Debugging
本文提出PolyDebug，一个语言无关但利用现有调试器的动态可扩展框架，通过DAP集成协调调试，以低成本支持多语言调试，并在C、JavaScript和Python上验证了其有效性与性能权衡。
2025-02-27 cs.PL
On Performance Debugging of Unnecessary Lock Contentions on Multicore Processors: A Replay-based Approach
锁已被广泛用作进程和线程之间有效的同步机制。然而，我们观察到大量的错误线程间依赖性（即，不必要的锁争用）存在于多核处理器上的程序执行期间，由此引起显著的性能开销。本文提出了一个性能调试框架，PERFPLAY，以促进全面和深入的理解不必要的锁争用的性能影响。我们的调试框架的核心技术是跟踪重放。PERFPLAY记录了程序的执行轨迹，在此基础上通过轨迹分析可以识别出不必要的锁争用。然后，我们提出了一种新的跟踪转换技术，将这些确定不必要的锁争在原来的跟踪到正确的模式，作为一个新的跟踪不必要的锁争。通过重放这两个跟踪，PERFPLAY可以量化不必要的锁争用对性能的影响。为了证明我们的调试框架的有效性，我们研究了五个现实世界的程序和PARSEC基准。我们的实验结果表明显着的性能开销不必要的锁争用，和PERFPLAY在识别性能关键的不必要的锁争用在实际应用中的有效性。
2015-04-21 cs.PL
An Assertion-Based Program Logic for Probabilistic Programs
概率程序的演绎验证研究已经考虑了基于期望的逻辑，其中前置条件和后置条件是状态上的实值函数，以及基于断言的逻辑，其中前置条件和后置条件是状态分布上的布尔谓词。这两种方法都发展了近40年，但今天它们有不同的地位。基于期望的系统已经成功地将许多复杂的案例研究形式化，而今天基于断言的系统具有更有限的表达能力，并且针对更简单的示例。我们目前Ellora，一个健全的和相对完整的断言为基础的程序逻辑，并证明其表现力通过验证几个经典的例子，随机算法使用的EasyCrypt证明助手的实现。Ellora为循环和对抗代码提供了新的证明规则，并支持比现有程序逻辑更丰富的断言。我们还表明，Ellora允许方便的推理复杂的概率概念，通过开发一个新的程序逻辑的概率独立性和分布规律，然后顺利地嵌入到Ellora。我们的工作表明，基于断言的方法并没有从根本上受到限制，并表明在基于断言的系统中，一些概念可能更容易推理。
2018-03-14 cs.LO cs.PL
Stepping Lazy Programs
消除懒惰的函数式程序带来了严重的挑战。为了支持命令式语言的“停止、检查和恢复”调试风格，一些调试工具放弃了惰性计算。其他调试器保留了惰性，但以一种可能使程序员感到困惑的方式呈现，因为评估的焦点以一种看似随机的方式跳跃。在本文中，我们介绍了一个补充工具，代数程序步进。代数步进器将计算显示为数学计算。代数单步执行对于初学者或刚接触惰性编程的程序员特别有用。从数学上讲，代数步进器将计算呈现为懒惰微积分的标准重写序列。我们的新的懒惰语义介绍了懒惰的评价作为一种形式的并行程序重写。它代表了Launchbury的基于存储的语义和通过参数共享的懒惰计算的简单公理化描述之间的折衷。最后，我们证明了步进的运行时机器正确地重建标准的重写序列。
2011-08-23 cs.PL
Extending programs with debug-related features, with application to hardware development
可重构硬件（如FPGA）的容量和可编程性多年来一直在稳步提高，但它们并不容易提供任何监控或调试运行程序的机制。这种机制需要写入程序本身。与CPU编程相比，这是使用临时方法和原始工具完成的。这使得可重构硬件的编程和调试变得复杂。我们介绍程序托管的可指导性（PhD），程序的扩展，在运行时解释方向命令，使调试，监控和分析。通常在硬件开发中，这些特性在编译时就被固定下来了。我们提出了一种语言的指导命令，指定其语义方面的一个简单的控制器，是嵌入式程序，并实现了一个原型，用于指导网络程序在硬件上运行。我们表明，这种方法提供了显着的灵活性，对硬件利用率和性能的影响较低。
2017-05-28 cs.PL
Generation of and Debugging with Logical Pre and Postconditions
本文介绍了SLAM系统提供的调试工具。SLAM系统包括i）规约语言，其使用面向对象的模型来集成代数规范和基于模型的规范。类操作是通过使用规则来定义的，每个规则都有逻辑上的前置条件和后置条件，但都有函数的味道。ii）一种开发环境，除了其他特征之外，该开发环境能够以高级面向对象语言生成可读代码。iii）生成的代码包括（部分）前置和后置条件作为断言，可以在程序的调试模式执行中自动检查。我们专注于最后一个方面。SLAM语言的表达能力足以描述许多有用的属性，这些属性被翻译成Prolog程序，该程序（通过适当的接口）与用户程序链接。程序的调试执行与负责检查属性的Prolog引擎交互。
2001-01-12 cs.PL cs.SE
Natural Hoare Logic: Towards formal verification of programs from logical forms of natural language specifications
形式化验证为软件的正确性提供了强有力的保证，这在安全或安全关键系统中尤为重要。霍尔逻辑是一种广泛使用的形式主义，用于以前置条件/后置条件断言的形式针对规范对软件进行严格验证。语义解析技术的进步和更高的计算能力使我们能够从自然语言文本中提取语义内容作为形式逻辑形式，具有越来越高的准确性和覆盖率。本文提出了一个基于霍尔逻辑的命令式程序形式化验证的形式化框架，该框架使用由自然语言断言的组合语义解析生成的逻辑形式。我们称这种推理方法为自然霍尔逻辑。这使得能够直接针对领域专家以自然语言指定的安全需求对软件进行形式化验证。我们认为这两个声明性断言的程序不变量和状态变化以及命令性断言，指定命令改变程序状态。我们将讨论如何推理方法可以扩展使用领域知识和实用的方法，防止语义分析器错误。
2021-03-04 cs.PL
Two automated techniques for analyzing and debugging Mpi-based programs
消息传递接口（MPI）是编写并行程序最常用的范例，因为它不仅可以在单个处理节点内使用，而且可以跨多个连接的节点使用。数据流分析的概念，技术和工具，需要理解和分析基于MPI的程序，以检测这些程序中出现的错误。在本文中，我们提出了两种自动化技术来分析和调试基于MPI的程序源代码。
2013-11-04 cs.DC cs.PL
Tracers for debugging and program exploration
EPFL（洛桑联邦理工学院）
本文提出通过追踪程序执行完整历史来改进调试方法，强调显示执行顺序而非语法顺序，探讨设计选择与初步结果。
2026-04-10 cs.HC cs.PL
Direct Interpretation of Functional Programs for Debugging
我们对长期存在的调试问题进行了另一次攻击。在探讨了为什么调试器没有像人们期望的那样广泛使用，特别是在函数式编程环境中，我们定义了调试器的特性，使其可用，从而广泛使用。我们提出了一个新的调试器OCaml的直接解释的程序源操作，允许打印出的程序的评估的各个步骤的初步工作。我们提出了OCamli，一个独立的解释器，并提出了一种机制，解释器可以集成到编译的可执行文件，允许程序的一部分被解释在相同的方式作为OCamli，而其余的程序本地运行。我们展示了这样的机制可能会创建一个源代码级的调试系统，具有可用的调试器的特性（如独立于其环境），因此最终可能会被期望适合广泛采用。
2019-05-16 cs.PL cs.SE
The Time-Space Complexity of Checking Multiple Assertions in Quantum Programs
University of Wisconsin–Madison（威斯康星大学麦迪逊分校）
研究检查量子程序中多个断言的时空复杂度，揭示报告所有断言结果需线性复杂度，而检测断言失败及识别首个失败断言仅需对数复杂度，还建立了相关复杂度的格局并通过案例研究验证，为量子程序员提供设计空间。
2026-07-14 cs.PL quant-ph
Support for Debugging Automatically Parallelized Programs
我们描述了一个系统，它简化了计算机辅助并行化工具产生的调试程序的过程。该系统使用相关的调试技术来比较串行和并行执行，以显示计算开始不同的地方。如果原始串行代码是正确的，则将通过比较来隔离由于并行化引起的错误。系统的主要目标之一是最小化用户所需的工作量。为此，调试系统使用由并行化工具产生的信息来驱动比较过程。特别地，调试系统依赖于并行化工具来提供关于变量可能已被修改的位置以及数组如何跨多个进程分布的信息。通过使用动态检测，用户的工作量也减少了。这允许我们修改程序执行，而不改变用户构建可执行文件的方式。使用动态插装还允许我们以细粒度的方式比较执行，并且仅在检测到差异时才涉及调试器。这减少了执行插装的开销。
2000-12-11 cs.PL cs.SE
Accurate Coverage Metrics for Compiler-Generated Debugging Information
针对优化程序调试信息不完整且现有覆盖率度量方法粗糙不可比的问题，提出可由工具计算的新度量标准，以激励语言实现提升调试质量。
2024-02-07 cs.PL cs.SE
A Framework for Debugging Java Programs in a Bytecode
在软件工程领域，程序分析和理解一直被认为是一个非常具有挑战性的任务，因为它需要专门的时间和精力。由于其静态特性，对源代码的分析有时可能相对容易，然而，后端代码（字节码），特别是在Java编程方面，分析起来很复杂。在本文中，我们提出了一种方法论的方法来理解Java程序的字节码。提出了一个Java字节码调试过程的框架。此外，我们讨论了调试过程中的字节码理解从简单的多语句方面的数据流分析。最后，我们提出了一个比较分析的字节码随着模拟的建议框架的调试过程
2019-04-29 cs.FL cs.PL cs.SE
Causal-Consistent Reversible Debugging: Improving CauDEr
本文扩展了 Erlang 因果一致可逆调试框架，使其直接支持源程序并融合用户驱动调试与重放调试，开发了新版工具 CauDEr。
2024-06-09 cs.PL
Extended Abstract - Model-Based Debugging of Java Programs
基于模型的推理是当前智能诊断系统研究的核心概念。它是基于这样的假设，即技术设备中的错误行为的来源可以通过描述某个应用领域的组件的基本属性的模型的存在来定位和识别。当关于由这些组件组成的系统的不当行为的实际数据可用时，可以使用独立于域的诊断引擎来推断系统的哪些部分对观察到的行为有贡献。本文介绍了应用程序的基于模型的方法来调试的Java程序编写的一个子集的Java。我们展示了一个简单的依赖模型，可以从一个程序，演示使用该模型的调试和减少所需的用户交互，给出了比较的功能依赖模型与程序切片，最后讨论了一些当前的研究问题。
2000-11-20 cs.PL cs.SE
MIO: Multiverse Debugging in the Face of Input/Output -- Extended Version with Additional Appendices
针对微控制器上非确定性程序的调试难题，本文提出MIO多元宇宙调试方法，支持广泛输入/输出操作，保证只探索常规执行可达状态，并在WARDuino上验证其可行性。
2025-09-08 cs.PL cs.SE
VeriFly: On-the-fly Assertion Checking via Incrementality
断言检查是程序员的一个非常宝贵的工具，它可以在动态语言（如Prolog）中发现许多类错误或验证它们的存在。对于Prolog程序员来说，这意味着能够拥有相关的属性，如模式，类型，确定性，非故障，共享，约束，成本等，检查并标记错误，而无需实际运行程序。这样的全局静态分析工具在软件开发周期中越早使用就越有用，并且快速的响应时间对于交互式使用是必不可少的。每次进行更改时，都要对软件项目进行全面而精确的语义分析，这可能会非常昂贵。在我们的静态分析和验证框架中，通过模块化和增量（上下文和路径敏感）分析的组合来解决这一挑战，该分析响应于不同粒度级别的程序编辑。我们描述了如何在一个集成开发环境（IDE）中的框架的组合，利用这种增量，以实现高水平的反应时，反映分析和验证结果的着色和工具提示直接在程序文本-该工具的VeriFly模式。我们所描述的具体实现是基于Emacs的，并且部分地重用了现成的“动态”语法检查工具（flycheck）。我们相信，类似的扩展也可以在其他成熟的开发环境中以较低的工作量进行复制。我们使用该工具的初步经验显示出非常有希望的结果，具有低延迟时间，在开发过程中为程序员提供早期，连续和精确的断言检查和其他语义反馈。该工具支持Prolog本地，以及其他语言的语义转换成霍恩子句。本文件正在考虑被TPLP接受。
2021-08-17 cs.PL
On-the-fly Query-Based Debugging with Examples
程序错误很难发现，因为在错误发生的时间和程序员发现错误的时间之间存在因果差距。虽然调试技术（如条件断点和数据断点）有助于在简单情况下找到错误原因，但在许多情况下，它们无法有效地弥合因果差距。基于查询的调试器为程序员提供了一个有效的工具，它通过在被调试程序运行时不断检查对象间的关系来提供即时的错误警报。为了使基于查询的调试器在程序执行中以便携式的方式，我们提出了高效的Java类文件插装，并讨论替代技术。虽然动态调试器的开销比基于查询的动态调试器高，但它提供了额外的交互能力和灵活性，同时保持了完全的可移植性。为了加快动态查询评估，我们的调试器在可移植的Java实现使用的组合，程序插装，加载时代码生成，查询优化，和增量重新评估。本文讨论了动态调试，并演示了基于查询的调试器应用程序调试Java煤气罐小程序以及SPECjvm 98套件应用程序。
2000-11-16 cs.PL cs.SE
A brief overview of the MAD debugging activities
并行和分布式程序是一个困难的活动，由于顺序错误的多样性，存在恶性效应，如竞争条件和死锁，以及必须处理的大量数据。这些问题由监视和调试环境MAD解决，它提供基于程序执行的图形表示的调试功能。MAD的目标应用程序是应用标准消息传递接口MPI的并行程序，该接口广泛用于高性能计算领域。MAD的亮点是交互式检查机制，包括分布式数组的可视化，图形化放置断点的可能性，监视器开销删除的机制，以及由于代码中的不确定性而发生的竞争消息的评估。
2000-12-16 cs.PL cs.SE
Execution replay and debugging
由于大多数并行和分布式程序在内部是不确定的--连续运行相同的输入可能会导致不同的程序流--因此，普通的循环调试技术是无用的。为了使用循环调试工具，我们需要一个记录执行信息的工具，这样就可以重放它进行调试。因为记录信息会干扰执行，所以我们必须限制信息量并保持信息的快速处理。本文包含了现有的执行重放技术和工具的调查。
2000-11-06 cs.PL cs.SE
VST-A: A Foundationally Sound Annotation Verifier
提出VST-A注解验证器，通过在Coq中分析控制流图并将C函数分解为直线型Hoare三元组，结合VST丰富的断言语言与形式化可靠性证明，实现了兼具自动化与高灵活性的基础程序验证。
2023-10-26 cs.PL
Abstract Diagnosis for Timed Concurrent Constraint programs
时间并发约束语言（Timed Concurrent Constraint Language，简称tccp）是一种基于简单但功能强大的并发约束范式Saraswat的并发逻辑语言。在这种范例中，存储作为值的概念被存储作为约束的概念所取代，这引入了与存储作为值的概念的一些差异。其他并发方法。在本文中，我们提供了一个通用的框架调试tccp程序。为此，我们首先提出了一个新的紧凑的，自底向上的语义的语言，非常适合于调试和验证的目的，在反应式系统的上下文中。我们还提供了一个抽象的语义，使我们能够有效地实现基于抽象解释的调试算法。给定一个tccp程序和一个行为规范，我们的调试方法自动检测程序是否满足规范。这与其他半自动调试方法不同，避免了提前提供症状的需要。我们通过介绍两个说明性的例子来展示我们的方法的有效性。我们选择一个特定的抽象域，并展示我们如何可以检测到一个程序是错误的。
2011-09-07 cs.LO cs.PL
Multi-Mode Debugging for FRP-Based Embedded Systems
Institute of Science Tokyo（东京科学大学）
针对Emfrp嵌入式应用的抽象鸿沟问题，提出多模式调试框架，结合源代码映射技术，可在Emfrp抽象级与C/C++ I/O级调试，经ESP32案例验证提升调试效率。
2026-09-30 cs.PL cs.SE
Stepwise Debugging of Answer-Set Programs
Technische Universität Wien（维也纳工业大学）；Universität Leipzig（莱比锡大学）
我们介绍了一个步进方法的答案集编程（ASP），允许调试答案集程序，是基于逐步应用的规则。类似于命令式语言中的调试，其中程序的行为是在逐步执行期间观察的，ASP的单步执行允许观察规则应用程序在计算答案集时的效果。虽然这种方法的灵感来自命令式编程中的调试，但由于ASP固有的非确定性和声明性，它在概念上与其他范例中的单步执行不同。特别是，与遵循严格控制流执行的命令式程序中的语句不同，在计算期间没有预先确定的顺序来考虑ASP中的规则。在我们的方法中，用户可以根据自己的直觉自由决定在下一步中考虑哪个规则是有效的。这样，可以将注意力集中在调试搜索空间中感兴趣的部分。通过揭示程序的实际语义和用户期望之间的差异，在单步执行期间检测错误。作为一个坚实的正式的基础，步进，我们开发了一个框架的计算答案集的程序。为了完全支持不同的求解器语言，我们建立了一个抽象的ASP语言，是足够一般的捕捉不同的求解器语言我们的框架。为此，我们利用抽象约束作为流行的语言结构，如聚合的一个既定的抽象。Stepping已在SeaLion中实现，SeaLion是一个ASP.我们使用一个示例场景来说明步进，并讨论SeaLion的步进插件。此外，我们阐述了方法方面和嵌入的ASP开发过程中的步进。
2017-05-18 cs.AI cs.LO cs.PL
ReduKtor: How We Stopped Worrying About Bugs in Kotlin Compiler
众所周知，缺陷定位是软件工程中的一个难题，特别是在编译器开发中，将输入程序减少到最小的复制示例是有益的;这种技术通常称为delta调试。另一个问题是，每种新的程序设计语言都有自己独特的怪癖和弱点，这使得完全有效地重用现有的工具和方法几乎是不可能的。在这篇经验论文中，我们解决了delta调试问题w.r.t. Kotlin，一种来自JetBrains的相对较新的程序设计语言。我们的方法是基于程序切片，分层增量调试和Kotlin特定转换的新组合，它们相互协同。我们在一个名为ReduKtor的原型中实现了它，并对合成和真实的Kotlin程序进行了广泛的评估;我们还将其性能与经典的delta调试技术进行了比较。评估结果支持我们的Kotlin delta调试方法的实际可用性，也表明了使用语言无关和语言特定技术来实现最佳还原效率和性能的重要性。
2019-09-16 cs.PL cs.SE
Spreadsheet Debugging
本文针对电子表格程序的质量问题，在基于区间的测试方法基础上提出一种故障追踪技术，利用数据流信息和单元格标记定位最具影响力的故障单元格。
2008-01-28 cs.PL cs.SE
Debugging Trait Errors as Logic Programs
针对 Rust 中 trait 约束规模增大导致编译器诊断失效的问题，提出一种 trait 调试器，通过从 trait 求解器提取并交互式可视化证明树，帮助开发者在任意领域和规模下诊断 trait 错误。
2023-09-10 cs.HC cs.PL
Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs
需要一个带有量子变量的一阶逻辑作为断言语言，用于指定和推理量子程序的各种属性（例如正确性）。令人惊讶的是，这样的逻辑在文献中缺失，现有的一阶Birkhoff-von Neumann量子逻辑只处理经典变量和它们的量化。在本文中，我们填补了这一空白，通过引入一阶扩展的Birkhoff-von Neumann量子逻辑与泛量词和存在量词的量子变量。给出的例子表明，我们的逻辑特别适合于指定量子计算和量子信息中研究的一些重要性质。我们进一步将此逻辑作为断言逻辑纳入量子霍尔逻辑中，使其能起到类似于经典霍尔逻辑中的一阶逻辑和分离逻辑中的BI-逻辑的作用。特别是，我们展示了它如何可以用来定义和推导量子概括的一些适应规则，已被应用于显着简化验证的经典程序。预计本文中定义的断言逻辑-一阶量子逻辑与量子变量-可以与各种量子程序逻辑相结合，作为一个坚实的逻辑基础上，验证工具可以建立使用证明助手，如Coq和Isabelle/HOL。
2022-05-04 cs.LO cs.PL quant-ph
Explaining Counterexamples with Giant-Step Assertion Checking
在程序的演绎验证过程中，识别证明失败的原因是困难的：它可能是由于程序中的不正确，程序注释中的不完整性，或者证明器的不完整性。解决证明失败所需的更改取决于其类别，但证明器无法提供任何分类帮助。当使用SMT求解器来履行证明义务时，该求解器可以从失败的尝试中提出一个模型，从中可以导出一个可能的反例。但反例可能是无效的，在这种情况下，它可能会增加更多的混乱而不是帮助。为了检查反例的有效性和分类证明失败，我们提出了两种不同的语义下的运行时断言检查（RAC）执行之间的比较，使用反例作为一个预言。第一次RAC执行遵循正常的程序语义，违反程序注释表示程序中存在错误。第二个RAC执行遵循一个新的“giant-step”语义，它既不执行循环，也不执行函数调用，而是从oracle中检索返回值和修改变量的值。只有在巨步执行下才能观察到的程序注释的违反表征了程序注释的不完整性。我们实现了这种方法在Why 3平台的演绎程序验证和评估它使用的例子从以前的文献。
2021-08-06 cs.LO cs.PL
Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
Max-Planck Institute for Security and Privacy (MPI-SP)（马克斯·普朗克安全与隐私研究所）；IMDEA Software Institute（IMDEA软件研究所）；Key Laboratory of System Software (Chinese Academy of Sciences)（中国科学院系统软件重点实验室）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；Eidgenössische Technische Hochschule (ETH) Zürich（苏黎世联邦理工学院）；Ludwig-Maximilians-Universität München（慕尼黑大学）；Munich Center for Quantum Science and Technology (MCQST)（慕尼黑量子科学与工程中心）
提出用于无限维量子及经典-量子程序的完整关系逻辑，以自伴无界线性关系建模断言，支持定量与定性推理，并通过收敛定理和无限维对偶定理证明完备性。
2026-07-02 cs.LO cs.PL quant-ph
Bugs4Q: A Benchmark of Real Bugs for Quantum Programs
可重现错误和修复的实际基准对于调试和测试方法的良好实验评估至关重要。然而，到目前为止，还没有合适的基准测试套件可以系统地评估量子程序的调试和测试方法。本文提出了Bugs4Q，一个基准的36个真实的，手动验证Qiskit错误从四个流行的Qiskit元素（Terra，Aer，Awis，和Aqua），补充测试用例再现错误的行为。Bugs4Q还提供了访问Qiskit程序的错误版本和修复版本以及执行相应测试用例的接口，便于对Qiskit程序调试和测试工具进行可重复的实证研究和比较。Bugs4Q可在https://github.com/Z-928/Bugs4Q上公开获取。
2021-09-20 cs.PL cs.SE
An Axiomatic Approach to Detect Information Leaks in Concurrent Programs
在并发环境中实现流安全性是极具挑战性的，主要是由于执行的不确定性。从安全角度来看，如果顺序线程通过公开可观察的语句（如print、sleep、delay等）披露控制位置，则会进一步加剧这种困难。受以前的作品，使用经典的霍尔风格的证明系统建立分布式（实时）程序的正确性的启发，在本文中，我们描述了一种方法，通过引入泄漏断言在可观察的程序点，发现并发程序中的信息泄漏。类似于经典的断言，我们演示了如何在并发上下文中检测到信息泄漏。据我们所知，这是第一个这样的工作，使不同的概念，不干涉功能和安全方面使用的整合。虽然这种方法在经典意义上是合理且相对完整的，但它允许使用算法技术，使程序员能够提出泄漏断言，从而检查敏感应用程序中的信息泄漏。
2021-03-03 cs.CR cs.PL
Inferring multiple helper Dafny assertions with LLMs
INESC TEC, Faculty of Engineering, University of Porto（葡萄牙波尔图大学工程学院INESC TEC）；Computer Science Department of Carnegie Mellon University（卡内基梅隆大学计算机科学系）
本文研究使用LLM自动推断Dafny程序中缺失的辅助断言，提出结合LLM预测与错误消息启发式的混合方法改进错误定位，并在新工具DAISY中实现，有效降低了形式化验证的证明工程工作量。
2025-10-31 cs.AI cs.LO cs.PL
TraceDiff: Debugging Unexpected Code Behavior Using Trace Divergences
程序合成的最新进展提供了在大规模编程教室中自动调试学生提交并生成个性化反馈的方法。当自动生成编程作业的反馈时，一个关键的挑战是设计教学上有用的提示，这些提示与教师给出的手动反馈一样有效。通过对132篇网络问答帖中教师暗示行为的分析，我们确立了有效反馈设计应遵循的三条设计原则。基于这些准则，我们开发了一个反馈系统，利用程序合成和可视化技术。我们的系统比较了不正确代码和固定代码的动态代码执行，并强调了错误如何导致行为的差异，以及不正确的代码跟踪偏离预期的解决方案。从我们的研究结果表明，我们的系统使学生能够检测和修复错误，没有被学生使用另一个现有的可视化调试工具。
2017-08-12 cs.CY cs.HC cs.PL
Debugging Machine Learning Tasks
University of Colorado, Boulder（科罗拉多大学博尔德分校）；Microsoft Research（微软研究院）；Carnegie Mellon University（卡内基梅隆大学）；IBM Research（IBM研究院）
与具有大量代码的传统程序（例如操作系统或字处理器）不同，机器学习任务使用具有相对少量代码（在机器学习库中编写）但具有大量数据的程序。就像传统程序的开发人员调试代码中的错误一样，机器学习任务的开发人员调试并修复数据中的错误。然而，与用于检测和修复代码中的错误的算法和工具相比，用于调试和修复数据中的错误的算法和工具不太常见。在本文中，我们认为分类任务中的错误训练数据导致错误分类的测试点，并提出了一种自动化的方法来找到这种错误分类的根本原因。我们的根本原因分析基于Pearl的因果关系理论，并使用Pearl的PS（充分概率）作为评分指标。我们的实现，Psi，编码PS的计算作为一个概率程序，并使用最近的工作概率程序和概率程序的转换（连同灰箱模型的机器学习算法），以有效地计算PS。Psi能够在感兴趣的数据集中识别数据错误的根本原因。
2016-03-23 cs.AI cs.LG cs.PL
CUDABeaver: Benchmarking LLM-Based Automated CUDA Debugging
University of Minnesota（明尼苏达大学）
提出CUDABEAVER基准，通过协议条件指标pass@k(M,C,A)评估LLM修复CUDA代码的能力，揭示性能损失容忍度对成功率的影响。
2026-05-26 cs.LG cs.PL cs.SE
Declarative Diagnosis of Floundering
许多逻辑程序设计语言都有延迟原语，允许协同编程。这引入了一类错误症状--当计算想要成功或有限失败时，计算可能会陷入困境。对于并发逻辑程序，这通常称为死锁。类似地，约束逻辑程序可能无法调用某些约束求解器，因为变量没有被充分地实例化或约束。迄今为止，诊断此类故障的注意力相对较少。由于延迟原语影响程序的过程性而不是声明性视图，因此可以预期调试必须考虑交错执行的通常复杂的细节。然而，最近的工作语义提出了另一种方法。在本文中，我们将展示如何声明式调试范式可以用来诊断意外的挣扎，绝缘的复杂性执行的用户。关键词：逻辑程序设计，协同程序设计，延迟，调试，挣扎，死锁，约束
2007-11-01 cs.PL cs.SE
WatChat: Explaining perplexing programs by debugging mental models
MIT（麻省理工学院）；Cambridge（剑桥大学）；Brown（布朗大学）；Cornell（康奈尔大学）；UCSD（加州大学圣地亚哥分校）
本文提出 WatChat 框架，将用户对语言/API 的误解建模为反事实错误语义并用程序综合调试，从而解释程序困惑行为，在 JavaScript 与 Git 领域优于现有语言模型。
2024-10-02 cs.AI cs.HC 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
Verifying Array Manipulating Programs by Tiling
形式化验证在循环中操作数组的程序的属性在计算上是具有挑战性的。在本文中，我们专注于一个有用的类这样的程序，并提出了一种新的属性驱动的验证方法，首先推断数组访问模式的循环使用简单的逻辑，然后使用这些信息来证明普遍量化的断言组合数组。具体来说，我们确定在一个循环中的数组访问模式的瓦片，并使用瓦片信息，以减少在一个循环结束时，检查一个量化的断言的问题，一个归纳参数，检查只有一个切片的断言的循环体的一个单一的迭代。我们表明，这种方法可以扩展到程序顺序组成的循环和嵌套循环以及。我们已经在一个名为Tiler的工具中实现了我们的方法。初步实验表明，Tiler优于几个国家的最先进的工具在一套有趣的基准测试。
2017-10-04 cs.LO cs.PL cs.SE
ChatDBG: Augmenting Debugging with Large Language Models
University of Massachusetts Amherst（马萨诸塞大学阿默斯特分校）；Amazon Web Services（亚马逊网络服务）；Williams College（威廉姆斯学院）
ChatDBG是一个集成大型语言模型的AI调试助手，通过与调试器协作对话，实现根因分析、错误解释和自动修复，显著提升调试效率，单次查询修复率达67%。
2025-06-19 cs.AI cs.LG cs.PL
