Enhancing Dynamic Symbolic Execution by Automatically Learning Search Heuristics
我们提出了一种技术，自动生成搜索引擎的动态符号执行。动态符号执行中的一个关键挑战是如何有效地探索程序的执行路径，以在有限的时间预算内实现高代码覆盖率。动态符号执行采用搜索启发式来解决这一挑战，这有利于探索最有可能最大化最终覆盖率的特定类型的路径。然而，手动设计一个好的搜索启发式是不平凡的，通常以次优和不稳定的结果结束。本文的目标是通过自动学习搜索策略来克服动态符号执行的这一缺点。我们定义了一类搜索启发式，即一个参数搜索启发式，并提出了一个算法，有效地找到一个最佳的启发式每个主题程序。使用工业强度符号执行工具（例如，KLEE）表明，我们的技术可以成功地生成搜索引擎，显着优于现有的手工制作的搜索引擎在分支覆盖率和错误发现方面。
2019-07-23 cs.SE
Presentation: SymDefFix -- Sound Automatic Repair Using Symbolic Execution
在本演示中，我们介绍了我们的基于约束的修复方法，称为SymDefFix。SymDefFix基于ExtractFix [3]，并取代了ExtractFix的动态分析步骤，以检测错误并在具有符号执行的输入程序中找到潜在的修复位置。我们首先简要介绍ExtractFix的动机和修改，然后用一个例子来演示它。
2022-09-08 cs.SE
Shadow Symbolic Execution with Java PathFinder
回归测试确保软件系统在发展时仍然正确执行，并且更改不会引入意外的副作用。然而，创建显示不同行为的回归测试用例需要大量的工作。一个解决方案是影子符号执行的想法，最初基于KLEE为C编写的程序实现，它采用新旧程序的统一版本，并执行由具体值指导的符号执行，以探索改变的行为。在这项工作中，我们将影子符号执行的想法应用到Java程序中，因此，提供了一个扩展的Java Path（JPF）项目执行影子符号执行Java字节码。该扩展已应用于JPF测试类中的几个主题，在这些主题中，它成功地生成了暴露回归测试相关分歧的测试输入。
2018-02-05 cs.SE
Distributed Symbolic Execution using Test-Depth Partitioning
符号执行是一种经典的系统错误发现技术，近年来已经有了很多应用，但仍然难以扩展。最近的工作介绍了范围内的符号执行分配不同的工人之间的符号执行任务，最小的通信开销使用测试输入。然而，每个工人被限制只能执行深度优先搜索。本文介绍了一种新的测距方法，称为测试深度分区，它允许工人采用不同的搜索策略，而不损害整体搜索的完整性。实验结果表明，该方法为分布式符号执行提供了一种更灵活的测距解决方案。测试深度分区背后的核心思想是使用测试深度对来定义执行空间中的区域。这样的对表示部分路径或前缀，并且它消除了如在先前测距方案中的情况那样对确定边界的完整测试的需要。此外，不同的工作者可以自由地选择所选择的搜索策略，而不影响整个系统的功能。测试深度划分是使用KLEE，一个著名的符号执行工具。初步结果表明，该方案可以证明是一个有效的工具，以加快符号执行。
2021-06-03 cs.SE
Verifying a Sparse Matrix Algorithm Using Symbolic Execution
针对科学软件复杂且易有细微错误的问题，提出用符号执行编写类似单元测试的测试以提供更强验证保证，并应用于稀疏矩阵算法。
2025-10-15 cs.SE
Badger: Complexity Analysis with Fuzzing and Symbolic Execution
涉及模糊测试和符号执行的混合测试方法在实现高代码覆盖率、发现各种软件应用程序中的细微错误和漏洞方面显示出有希望的结果。在本文中，我们描述獾-一种新的混合方法的复杂性分析，发现漏洞时发生的最坏情况下的时间或空间复杂度的应用程序是显着高于平均情况的目标。Badger使用模糊测试来生成一组不同的输入，其目的不仅是增加覆盖率，而且还与每个路径相关联的资源相关的成本。由于模糊可能无法执行深程序路径，由于其有限的知识的条件，影响这些路径，我们补充了分析与符号执行，这也是定制的搜索路径，增加资源相关的成本。符号执行特别擅长生成满足各种程序条件的输入，但它本身会遭受路径爆炸。因此，獾使用模糊和象征性执行串联，以利用他们的好处，克服他们的弱点。我们实现了我们的方法分析的Java程序，基于Kelinci和Symbolic Pathwords。我们在Java应用程序上评估了Badger，结果表明，与模糊或符号执行相比，我们的方法在生成最坏情况的执行方面要快得多。
2018-06-08 cs.SE
Killing Stubborn Mutants with Symbolic Execution
我们引入SeMu，一种动态符号执行技术，它生成能够杀死顽固突变体（经过合理数量的测试后仍未被检测到的可识别突变体）的测试输入。SeMu的目标是通过增量搜索原始版本和突变版本之间的不同程序行为来进行突变传播（触发程序输出的错误状态）。我们将突变体杀死问题建模为程序符号树中特定区域内的符号执行搜索。在这个框架中，搜索区域由允许可扩展和具有成本效益的突变体杀死的参数定义和控制。我们将SeMu集成到KLEE中，并尝试了Coreutils（符号执行研究中经常使用的基准）。我们的研究结果表明，我们的建模在突变体杀伤中起着重要作用。也许更重要的是，我们的研究结果还表明，在两小时的时间限制内，SeMu杀死了37%的顽固突变体，KLEE没有杀死任何突变体，而突变体感染策略（以前的研究建议的策略）杀死了17%。
2020-01-09 cs.SE
Regression Testing of Virtual Prototypes Using Symbolic Execution
近年来，虚拟平台和虚拟原型技术在电子企业中被广泛应用，以加速软件开发。实践证明，这些技术可以大大缩短产品上市时间，提高产品质量。一个挑战是如何测试和验证虚拟原型。在本文中，我们提出了如何进行回归测试的虚拟原型在不同版本中使用符号执行。假设我们有旧版本和新版本的虚拟原型，我们首先对新版本应用符号执行并收集所有路径约束。然后，收集路径约束用于指导旧版本的符号执行。对于探索的每个路径，我们比较两个版本之间的设备状态，以检查它们的行为是否相同。我们已经将这种方法应用于广泛使用的虚拟原型，并检测到许多差异。实验结果表明，该方法是有效的。
2016-01-22 cs.SE
S$^2$F: Principled Hybrid Testing With Fuzzing, Symbolic Execution, and Sampling
College of Computer Science and Electronic Engineering, Hunan University（湖南大学计算机科学与电子工程学院）；National University of Defense Technology（国防科技大学）
S$^2$F通过结合模糊测试、符号执行和采样，提升混合测试效率，发现更多崩溃。
2026-01-15 cs.SE
PathFuzzing: Worst Case Analysis by Fuzzing Symbolic-Execution Paths
本文提出PathFuzzing方法，通过将程序转换为接受二进制路径编码的符号程序并应用进化模糊测试搜索高资源消耗路径，有效结合模糊测试与符号执行优势解决最坏情况分析问题，实验证明其优于基线方法。
2025-07-14 cs.SE
Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications
Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；UCAS（中国科学院大学）；Sch. of Computer Science & Sch. of Artificial Intelligence, Shanghai Jiao Tong University（上海交通大学计算机科学与技术学院与人工智能学院）；School of Computer Science, Peking University（北京大学计算机学院）；Beijing Institute of Control Engineering（北京控制工程研究所）
本文提出一种结合符号执行与LLMs的方法，自动生成形式化程序规范，提升程序理解与验证的精度和适用性。
2026-01-20 cs.SE
Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
符号执行是测试输入生成的一种成熟方法。尽管在数值域上取得了巨大的成功，现有的基于堆的程序的符号执行技术是有限的，由于缺乏一个简洁和精确的描述符号值在无界堆。在这项工作中，我们提出了一个新的符号执行方法的堆为基础的程序的基础上分离逻辑。我们的建议的本质是上下文敏感的惰性初始化，有效的测试输入生成的新方法。我们的方法在两个方面不同于现有的方法。首先，我们的方法是基于分离逻辑，这使我们能够准确地捕捉基于堆的程序的先决条件，使我们避免产生无效的测试输入。其次，我们只生成完全初始化的测试输入，这是更有用的，在实践中相比，那些部分初始化的测试输入所产生的最先进的工具。我们已经实现了我们的方法作为一个工具，称为Java Starcraft，并评估了一组程序与复杂的堆输入。实验结果表明，该方法显著减少了无效测试输入的数量，提高了测试覆盖率。
2019-09-16 cs.SE
State Merging with Quantifiers in Symbolic Execution
针对符号执行中状态合并的约束编码爆炸问题，提出基于路径约束相似结构动态分组、用量词编码合并结果的方法，搭配专用求解流程降低复杂度，实现了显著性能提升。
2023-08-24 cs.SE
Combining Dynamic Symbolic Execution, Machine Learning and Search-Based Testing to Automatically Generate Test Cases for Classes
本文讨论了一种自动生成面向对象程序测试用例的新技术。在现有技术中，生成足够多的完整测试用例集的问题尚未得到满意的解决。有多种技术可以自动生成测试用例（随机测试、基于搜索的测试等）。但每个人都有自己的弱点本文提出了一种结合动态符号执行、基于搜索的测试和机器学习的方法，有效地生成完整的类级测试集。通过一些实验获得的初步数据证实，我们正朝着正确的方向前进。
2020-05-19 cs.SE
A Symbolic Execution Algorithm for Constraint-Based Testing of Database Programs
在所谓的基于约束的测试中，符号执行是一种常见的技术，用作为命令式程序生成测试数据的过程的一部分。数据库在软件中无处不在，因此对操纵数据库的程序进行测试对于提高软件的可靠性至关重要。本文提出了一种基于约束的数据库程序测试的符号表示算法，并进行了实验评估。首先，我们描述了SimpleDB，一种形式语言，它提供了一个最小的和定义良好的语法和语义，以模拟程序和数据库之间的常见交互场景。其次，我们详细介绍了所提出的算法，符号执行的SimpleDB模型。该算法将SimpleDB程序视为对一组关系变量的操作序列，对数据库表和程序变量进行建模。通过将程序的这种关系模型与经典的静态符号执行相结合，该算法可以为程序的控制流图中的任何有限路径生成一组路径约束以进行测试。这些约束的解是程序的测试输入，包括数据库的初始内容。当相对于这些输入执行程序时，保证遵循生成约束的路径。最后，该算法进行了实验评估，使用有代表性的SimpleDB模型。
2015-01-23 cs.SE
WANA: Symbolic Execution of Wasm Bytecode for Cross-Platform Smart Contract Vulnerability Detection
许多流行的区块链平台都支持智能合约来构建分散的应用程序。然而，智能合约中的漏洞给最终用户带来了严重的经济损失。对于EOSIO区块链平台，有效的漏洞检测器仍然有限。此外，现有的漏洞检测工具只能支持一个区块链平台。在这项工作中，我们提出了WANA，一个基于WebAssembly字节码符号执行的跨平台智能合约漏洞检测工具。此外，WANA提出了一组测试预言机，以检测基于WebAssembly字节码分析的EOSIO和以太坊智能合约中的漏洞。我们的实验分析表明，WANA可以高效地检测EOSIO和以太坊智能合约中的漏洞。
2020-08-05 cs.SE
Towards Symbolic Pointers Reasoning in Dynamic Symbolic Execution
动态符号执行是一种广泛用于自动化软件测试的技术，旨在探索执行路径和检测程序错误。一个混合的方法最近变得普遍，当符号执行的主要目标是帮助模糊增加程序的覆盖率。符号执行器可以反转的分支越多，它对模糊器就越有用。程序控制流通常依赖于内存值，这些内存值是通过从用户输入计算地址索引而获得的。然而，大多数DSE工具不支持这种依赖关系，因此它们会错过一些所需的程序分支。我们实现了符号地址推理的内存读取在我们的动态符号执行工具Sydr。可能的存储器访问区域是通过分析存储器地址符号表达式，或二进制搜索与SMT求解器确定。我们提出了一种增强的线性化技术来模拟内存访问。在程序集上比较了不同的内存建模方法。我们的评估表明，符号地址处理允许发现新的符号分支，并增加程序覆盖率。
2022-03-22 cs.CR cs.SE
Automatically Generating Test Cases for Safety-Critical Software via Symbolic Execution
基于符号执行的自动测试生成有利于系统地测试安全关键软件，方便测试工程师追求认证标准规定的严格测试要求，同时控制测试过程的成本。同时，安全关键软件的开发通常受到禁止被认为降低程序安全性的语言特征的程序设计语言或编码约定的限制，例如，它们不允许动态内存分配和可变长度数组，限制了循环的使用方式，禁止递归，并限制了控制条件的复杂性。事实上，这些语言特征也是最先进的基于符号执行的测试生成方法的主要效率障碍。本文为一类重要的工业安全关键系统提供了新的证据，证明了符号执行生成测试用例的有效性。我们特别关注的SCADE，主要采用基于模型的开发语言的安全关键的嵌入式软件，我们报告的案例研究中，我们利用符号执行自动生成测试用例的一组安全关键的程序在SCADE开发。为此，我们介绍了一种新的测试生成器，我们在最近的工业项目中开发的测试安全关键的铁路软件写在SCADE，我们报告我们的经验，使用此测试生成器测试一组SCADE程序，属于发展的车载信号单元的高速铁路。结果提供经验证据表明，符号执行确实是一种可行的方法，为我们的案例研究中考虑的安全关键程序生成高质量的测试套件。
2022-09-22 cs.SE
Path-optimal symbolic execution of heap-manipulating programs
University of Milano-Bicocca（米兰比可卡大学）
本文提出POSE算法，通过实现堆操作程序的路径最优性，提升符号执行效率。
2026-01-14 cs.LO cs.SE
cozy: Comparative Symbolic Execution for Binary Programs
本研究提出二进制差异分析工具cozy，基于angr符号执行框架寻找补丁前后二进制的兼容终态并对比差异，配套网页可视化界面辅助微补丁验证。
2025-03-31 cs.SE
Test Wars: A Comparative Study of SBST, Symbolic Execution, and LLM-Based Approaches to Unit Test Generation
本研究对比了SBST工具EvoSuite、符号执行工具Kex与LLM测试生成工具TestSpark在GitBug Java数据集上的表现，发现LLM方法变异得分更优但覆盖率、故障检测能力弱于传统方法，且对被测类规模更敏感。
2025-01-17 cs.SE
Interoperability-Guided Testing of QUIC Implementations using Symbolic Execution
网络协议（如QUIC）标准化的主要原因是确保实现之间的互操作性，这是一项具有挑战性的任务。手动测试目前用于测试不同的现有实现的互操作性，但鉴于网络协议的复杂性，很难涵盖所有可能的边缘情况。最先进的自动化软件测试技术，如符号执行（Symbolic Execution，SymbEx），已经证明自己能够分析复杂的真实世界的软件，并发现难以检测的错误。我们提出了一种基于SymEx的方法来发现QUIC实现中的互操作性问题，并在分析picoquic和QUANT互操作性的案例研究中探索其优点。我们发现，虽然SymEx能够分析不同实现之间的深层交互，并发现了几个错误，为了实现有效的互操作性测试，实现需要提供有关其当前协议状态的额外信息。
2018-11-29 cs.SE
Compositional Fuzzing Aided by Targeted Symbolic Execution
近年来，由于其快速的路径覆盖引导的输入变异策略，引导模糊已经能够发现现实世界中的软件中的许多新的漏洞。然而，大多数模糊器无法在程序的更深部分实现高覆盖率。此外，模糊器严重依赖于种子输入的多样性，通常是手动提供的，以便能够产生有意义的结果。在本文中，我们提出了野火，一种新的开源组合模糊框架。Wildfire通过模糊化C程序中的孤立函数来发现漏洞，然后使用有针对性的符号执行来确定利用这些漏洞的可行性。基于我们对23个开源源程序（近100万个）的评估，我们表明，由于覆盖率的增加，Wildfire比基线符号执行和模糊工具以及最先进的覆盖率引导工具发现了更多的真阳性结果，而这些工具所花费的分析时间只有10%。此外，Wildfire还发现了许多其他潜在的漏洞，这些漏洞的可行性可以通过组合来确定，以确认它们是否是误报。Wildfire还可以复制所有已知的漏洞，并在三个开源库中发现了几个以前未知的漏洞。
2019-10-11 cs.SE
Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery
University of California, Santa Barbara（加州大学圣塔芭芭拉分校）
SAILOR结合静态分析与LLM合成自动构建符号执行Harness，通过三个阶段发现内存安全漏洞，实验表明其在大规模代码库中显著提升漏洞检测效率。
2026-04-07 cs.CR cs.SE
Combining static analysis and dynamic symbolic execution in a toolchain to detect fault injection vulnerabilities
通过审计进行认证，可以确保关键嵌入式系统的安全。这需要审查其关键组件并检查危险的执行路径。后一项任务需要使用专门的工具，这些工具允许探索和重放执行，但在时间和代码知识有限的审计环境中也难以有效使用。故障分析尤其棘手，因为攻击者可能会主动影响执行，使一些常用方法无法使用，并以指数方式增加可能的执行路径。在这项工作中，我们提出了一种新的方法，减少了故障注入点的数量，认为只有最相关的相对于一些安全属性，以减轻这些问题。我们使用快速和强大的静态分析来检测注入点，并断言其影响。然后采用更精确的动态/符号方法来验证攻击路径。通过这种方式，发现攻击所需的洞察力减少了，动态方法可以更好地扩展到实际大小的程序。我们的方法被实现到一个工具链的基础上Frama-C和KLEE和验证WooKey，由法国国家网络安全局提出的案例研究。
2023-03-07 cs.SE
Benchmarking Symbolic Execution Using Constraint Problems -- Initial Results
IIT Kanpur（印度理工学院坎普尔分校）；National University of Singapore（新加坡国立大学）
符号执行是一种功能强大的bug发现和程序测试技术。它可以成功地发现真实代码中的bug。核心推理技术使用约束求解、路径探索和搜索，这些也是用于解决组合问题的相同技术，例如，有限域约束满足问题。我们提出CSP实例作为更具挑战性的基准来评估符号执行中核心技术的有效性。我们将CSP基准转换为适合测试符号执行工具的推理能力的C程序。从一个单一的CSP P，我们转换P取决于转换选择到不同的C程序。使用KLEE、Tracer-X和LLBMC工具进行的初步测试显示，转换和求解器选择在运行时存在很大差异。我们的C基准测试有效地显示了现有符号执行工具的局限性。这项工作的动机是，我们相信这种形式的基准可以刺激符号执行引擎中改进的核心推理的开发和工程。
2020-01-22 cs.AI cs.SE
Enhancing Reuse of Constraint Solutions to Improve Symbolic Execution
约束求解重用是节省符号执行中约束求解时间的有效途径。大多数现有的重用方法是基于语法或语义等价的约束;例如，绿色框架是能够重用的约束，具有不同的表示，但语义等价，通过规范化的约束到语法等价的范式。然而，语法/语义等价并不是重用的必要条件--有些约束在语法或语义上并不等价，但它们的解决方案仍然具有重用的潜力。现有的方法无法识别和重用这些约束。在本文中，我们提出了GreenTrie，一个扩展的绿色框架，它支持约束重用的基础上的逻辑蕴涵关系的约束。GreenTrie提供了一个名为L-Trie的组件，它将约束和解决方案存储到try中，并通过约束的隐含偏序图进行索引。L-Trie能够对给定的约束进行逻辑约简和逻辑子集和超集查询，以检查先前解决的约束的重用。我们报告的GreenTrie对原来的绿色框架，这表明我们的扩展实现了更好的重用约束求解结果，节省了显着的符号执行时间的实验评估结果。
2015-01-28 cs.SE
Can LLMs Recover Program Semantics? A Systematic Evaluation with Symbolic Execution
本文研究LLMs通过符号执行制品微调能否有效去混淆程序，发现GPT-4.1-mini在去混淆效果上最佳，结合KLEE制品能提升语义保留和编译成功率。
2025-11-24 cs.SE
Evaluating Manual Intervention to Address the Challenges of Bug Finding with KLEE
符号执行已经显示出其在软件中发现安全相关缺陷的能力，但面临着重大的可扩展性挑战。人们普遍认为，专家的人工干预可以帮助减轻这些限制因素。然而，很少有正式的调查这一想法。在本文中，我们提出了我们的经验，应用KLEE符号执行引擎的一个新的错误语料库，并使用人工干预，以减轻遇到的问题。我们的贡献是（1）半翅目，一个新的语料库的130多个错误，在现实世界的软件，（2）一个全面的评估KLEE符号执行引擎的半翅目与经常发生的软件模式的分类是有问题的符号执行，和（3）评估手动缓解旨在解决符号执行的根本问题。我们的经验表明，在许多情况下，手动干预可以增加代码覆盖率和bug检测。然而，这不是一个银弹，我们讨论它的局限性和遇到的挑战。
2018-05-09 cs.SE
Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts
在软件测试中最大化代码覆盖率的一种有效方法是通过动态符号执行$-$，这是一种使用约束求解来系统地探索程序状态空间的技术。我们介绍了一个名为Manticore的开源动态符号执行框架，用于分析二进制文件和以太坊智能合约。Manticore灵活的架构使其能够支持传统和异国情调的执行环境，其API允许用户自定义他们的分析。在这里，我们将讨论Manticore的架构，并展示我们用于为商业客户查找错误和验证代码正确性的功能。
2019-11-18 cs.CR cs.SE
Directed Symbolic Execution for Vulnerability Discovery: An LLM-Guided Approach in KLEE
Kyushu University（九州大学）
研究针对符号执行的路径爆炸问题，提出基于KLEE的KLEECopilot方法，用大语言模型引导定向符号执行，标记潜在漏洞代码、指导路径优先级并集成循环退出优先级，相比基线提升显著，各组件对有效性有贡献。
2026-07-27 cs.SE
TracerX: Dynamic Symbolic Execution with Interpolation
动态符号执行（DSE）是一种重要的程序测试方法。DSE上的一个重要系统是KLEE，它输入一个带有符号变量的C/C++程序，将其编译成LLVM，然后使用指定的回溯策略仿真LLVM的执行路径。符号执行的主要挑战是路径爆炸。抽象学习的方法已经被用来解决这个问题。这里的关键步骤是计算插值来表示学习的抽象。本文提出了一种新的插值算法，并在KLEE系统上实现。主要目标是解决路径爆炸问题，追求代码渗透：证明一个目标程序点是可达或不可达。也就是说，我们的重点是核查。我们发现，尽管计算插值的开销，修剪的符号执行树插值提供往往带来显着的整体效益。然后，我们对KLEE进行了全面的实验评估，以及对一个著名的系统，是基于静态符号执行，CBMC。我们的初步实验表明，代码渗透成功率达到了一个新的水平，特别是当目标难以确定时。二次实验表明，我们的实现是有竞争力的测试。
2020-12-01 cs.PL cs.SE
Symbolic Execution for Verification
在以前的工作中，我们提出了一种符号执行方法，该方法从程序的具体模型开始，但只有当这些都是不相关的使用插值逐步抽象的细节。在本文中，我们扩展的技术来处理无界循环。其核心思想是通过循环展开过程逐步发现最强的不变量。这种技术的关键特征，称为极大极小算法，是智能回溯，直接搜索下一个不变。然后，我们提出了我们的符号执行方法和主要基于抽象细化（CEGAR）的主流技术之间的主要差异的分析。最后，我们评估我们的技术对现有的国家的最先进的系统。
2011-03-10 cs.PL cs.SE
SEDCoT: Enhancing LLM-Based COBOL Code Translation via Symbolic Execution and Delta Debugging
University of Lugano（卢加诺大学）；Technical University of Munich（慕尼黑工业大学）；University of Augsburg（奥格斯堡大学）
针对COBOL代码翻译难题，提出SEDCoT框架。先利用大语言模型初译，再结合符号执行与大语言模型指导生成测试套件修复语义差异，最后用增量调试最小化失败测试，提升翻译性能与可读性。
2026-09-02 cs.SE
Strong Optimistic Solving for Dynamic Symbolic Execution
动态符号执行（DSE）是自动化程序测试和缺陷检测的一种有效方法。通过对复杂分支的探索，提高了混合模糊的代码覆盖率。DSE工具沿着某些执行路径反转分支，并帮助模糊器检查以前不可用的程序部分。DSE经常面临过度约束和约束不足的问题。第一个导致显着的分析复杂性，而第二个导致不准确的符号执行。我们提出了强乐观的解决方法，消除无关的路径谓词约束的目标分支反演。我们消除这样的符号约束，目标分支是不控制dependenton.Therefore，我们单独处理符号分支，嵌套控制转移指令，通过控制超出父分支范围，例如返回，转到，休息等，我们实现了我们提出的方法在我们的动态符号执行工具Sydr。我们评估了强乐观策略，乐观策略，只包含最后一个约束否定，以及它们的组合。结果表明，策略组合有助于增加代码覆盖率或每分钟正确反转分支的平均数量。与其他配置相比，最好同时应用这两种策略。
2022-12-25 cs.CR cs.SE
Automated Reasoning and Detection of Specious Configuration in Large Systems with Symbolic Execution
配置错误是系统故障的主要原因。现有的解决方案集中于检测由用户错误引入的无效设置。但是，另一种继续困扰生产服务的错误配置类型是似是而非的配置--设置是有效的，但在生产中会导致意外的低性能。这样的错误配置是微妙的，所以即使是细心的管理员也可能无法预见它们。我们提出了一个工具，称为紫罗兰来检测这种错误配置。我们意识到似是而非的配置的关键是它导致一些缓慢的代码路径被执行，但不总是触发不良的性能影响。因此，Violet采用了一种新的方法，使用选择性符号执行来系统地推理配置参数的性能影响，它们的组合效果以及与输入的关系。Violet输出一个性能影响模型，用于自动检测不良配置设置。我们在四个大型系统上应用了Violet。为了评估Violet的有效性，我们收集了17个真实世界的似是而非的配置情况。维奥莉特发现了15个。Violet还识别了9种未知的似是而非的配置。
2020-10-05 cs.SE
Parallel Program Analysis on Path Ranges
本文提出一种将范围符号执行推广到任意程序分析的验证方法，通过将程序拆分为路径范围并行运行不同分析，并在CPAchecker上实现评估，发现并行化可加速验证但需引入工作窃取机制以提升效率。
2024-05-16 cs.SE
Python Symbolic Execution with LLM-powered Code Generation
本文提出 LLM-Sym 智能体，通过类型推断、检索与自我精化流水线将 Python 复杂路径约束转换为 Z3 代码，使入门级符号执行引擎可处理含 list 和复杂控制流的程序。
2024-09-14 cs.PL cs.SE
Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code
Key Lab of HCST (PKU), MoE, SCS, Peking University（北京大学信息科学技术学院，复杂系统管理与控制国家重点实验室）
本文提出Gordian框架，通过LLM生成轻量级鬼代码辅助SMT求解器处理对抗性代码，提升覆盖率和效率，减少LLM使用量。
2026-09-08 cs.PL cs.SE
SEAL: Symbolic Execution with Separation Logic (Competition Contribution)
Faculty of Information Technology, Brno University of Technology（布尔诺理工大学信息技术学院）；Faculty of Informatics, Masaryk University（马萨里克大学信息学院）
SEAL通过基于分离逻辑的模块化架构，实现了对无界链式数据结构程序的高效验证，在竞赛中表现出色。
2026-02-06 cs.SE
Symbolic Partial-Order Execution for Testing Multi-Threaded Programs
我们描述了一种多线程程序的系统测试技术。我们结合准最优偏序约简，一个国家的最先进的技术，解决路径爆炸，由于交错的非确定性，与符号执行来处理数据的非确定性。我们的技术迭代地和详尽地发现程序的所有执行。它使用偏序表示程序执行，并使用底层展开语义查找下一次执行。我们避免了使用截止事件的冗余程序痕迹的探索。我们实现了我们的技术作为KLEE的扩展，并评估了一组大型多线程C程序。我们的实验在memcached和GNU sort中发现了几个以前未发现的bug和未定义的行为，表明新方法能够在工业规模的基准测试中发现bug。
2020-07-22 cs.PL cs.SE
A Direct Symbolic Execution of SQL Code for Testing of Data-Oriented Applications
符号执行是一种能够自动生成测试输入（和输出）的技术，它在要测试的程序中执行一组执行路径。如果路径覆盖了被测代码的足够部分，则测试数据提供了程序实际行为的代表性视图，这尤其使得能够检测错误和纠正故障。关系数据库在软件中无处不在，但操作它们的代码片段的符号执行仍然是一个不小的问题，特别是因为这种数据库的复杂结构和SQL语句的复杂行为。在这项工作中，我们定义了一个直接的符号执行数据库操作代码，并将其与一个更传统的符号执行正常的程序代码。数据库表由关系符号表示，SQL语句由这些符号上的关系约束表示，符号表示程序的正常变量。基于这些原则的算法的符号执行的Java方法，实现业务用例的读写关系数据库，后者受到数据完整性约束。该算法被集成在一个测试生成工具，并在示例代码进行了实验。工具生成的约束的目标语言是SMT-Lib标准，使用的求解器是Microsoft Z3。结果表明，该方法能够在合理的时间内生成有意义的测试数据，包括有效的数据库内容。特别是，Z3求解器被证明是更可扩展的比合金求解器，在我们以前的工作中使用，解决关系约束。
2015-01-21 cs.DB cs.SE
Symbolic Execution for Deep Neural Networks
深度神经网络（DNN）越来越多地用于各种应用，其中许多应用具有实质性的安全性和安全性问题。本文介绍了DeepCheck，这是一种基于程序分析的核心思想，特别是符号执行的验证DNN的新方法。其思想是将DNN转换为命令式程序，从而使程序分析能够帮助DNN验证。然而，一个基本的翻译创建的程序是非常复杂的分析。DeepCheck为DNN的轻量级符号分析引入了新技术，并将其应用于图像分类的背景下，以解决DNN分析中的两个挑战性问题：1）识别重要像素（用于属性和对抗生成）;以及2）创建1像素和2像素攻击。使用MNIST数据集的实验结果表明，DeepCheck的轻量级符号分析为DNN验证提供了有价值的工具。
2018-07-27 cs.CR cs.SE
Coupling Distributed and Symbolic Execution for Natural Language Queries
Peking University（北京大学）
构建神经网络来使用自然语言查询知识库（表）是深度学习中的一个新兴研究课题。用于表查询的执行器通常需要多个执行步骤，因为查询可能具有复杂的结构。在以前的研究中，研究人员已经开发了完全分布式执行器或符号执行器表查询。分布式执行器可以以端到端的方式进行训练，但在执行效率和显式可解释性方面很弱。符号执行者在执行上是有效的，但是训练是非常困难的，尤其是在初始阶段。在本文中，我们建议耦合分布式和符号执行自然语言查询，其中的符号执行器是预先训练的分布式执行器的中间执行结果，在一步一步的方式。实验表明，我们的方法显着优于分布式和符号执行器，表现出高精度，高学习效率，高执行效率，高解释性。
2017-06-16 cs.AI cs.CL cs.LG
Integrating Symbolic Execution into the Fine-Tuning of Code-Generating LLMs
TU Darmstadt（图宾根大学）
本文研究利用符号执行增强奖励模型训练数据，并结合强化学习与直接偏好优化微调代码生成大语言模型，在代码质量评估上显著超越CodeRL基线，生成性能与CodeRL相当。
2025-05-05 cs.AI cs.SE
Agentic Planning for Symbolic Execution
Carnegie Mellon University（卡内基梅隆大学）
该研究提出智能体规划系统Agolic，利用早期符号执行运行的证据配置后续有界符号执行，在C/C++程序上平均覆盖3倍以上分支，覆盖更多分支及对比语料库未覆盖的分支，扩展了符号执行的实际覆盖范围。
2026-08-10 cs.AI cs.PL cs.SE
Can Large Language Models Simulate Symbolic Execution Output Like KLEE?
本研究探索GPT-4o能否模拟KLEE的符号执行输出以解决KLEE的资源消耗问题，测试其识别程序约束最多路径的能力，在100个C程序数据集上获约20%准确率，为LLM替代符号执行部分功能提供早期参考。
2025-11-11 cs.PL cs.SE
Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale
The University of Manchester（曼彻斯特大学）；RPTU Kaiserslautern（凯泽斯劳滕理工大学）
提出VerIbmc管道，结合符号不变量生成与本地开源语言模型及ESBMC验证工具，通过结构化的验证器反馈迭代优化，实现隐私保护且高效的循环不变量合成，在520个问题上达到86.4%的解决率。
2026-06-16 cs.SE
Can Large Language Models Reason About Complex Execution Paths? An Empirical Study on Python
Institute for Software Chinese Academy of Sciences（中国科学院软件研究所）；Peking University（北京大学）；University of Alberta（阿尔伯塔大学）；The University of Tokyo（东京大学）
本文实证研究大型语言模型在Python执行路径推理中的可行性，构建测试用例生成和缺陷分类任务，发现LLM能提升路径覆盖率，但强推理模型不一定优于弱模型。
2026-06-19 cs.SE
Enhancing Reliability of Symbolic Execution Tools for Smart Contract Analysis through Rule-Based False Positive Reduction
Lakehead University（拉科德湖大学）；United Arab Emirates University（阿联酋大学）；German Research Center for Artificial Intelligence（德国人工智能研究中心）；National University of Computer and Emerging Sciences（巴基斯坦国立计算机与新兴科学大学）
本文针对智能合约分析工具Mythril的误报问题，设计基于规则的误报减少方法，在不降低真实漏洞检测能力的前提下显著减少误报，提升了工具可靠性。
2026-08-12 cs.SE
Reviewing KLEE's Sonar-Search Strategy in Context of Greybox Fuzzing
符号执行和模糊测试的自动测试用例生成技术是学术界和工业界最广泛使用的发现漏洞的方法。然而，这两种方法都存在基本的缺点，这些缺点阻止它们实现高路径覆盖，因此，这可能导致在静态分析的数值尺度上发现漏洞。在这个演示文稿中，我们检查系统测试（SUTs）在功能的粒度级别，并假设实现更高的功能覆盖率（在程序中的功能执行至少一次）比，符号执行和模糊可能是发现更多的漏洞比这两个必要条件。我们将从KLEE的目标搜索策略的设计开始，声纳搜索，优先考虑通往目标功能的路径，而不是最大化程序中的整体路径覆盖。然后，我们将展示在函数级别（组合分析）检查SUT会发现比从单个入口点执行符号更多的漏洞。利用这一发现，我们将，然后，演示一个灰盒模糊方法，可以实现更高的功能覆盖率比符号执行。最后，我们将提出一个框架，以有效地管理漏洞和评估其严重性。
2018-03-13 cs.SE
SpecuSym: Speculative Symbolic Execution for Cache Timing Leak Detection
CPU高速缓存是现代处理器中有限但关键的存储组件，而高速缓存定时侧通道可能无意中通过物理可测量的定时方差泄漏信息。推测执行是一种重要的处理器优化，也是这种差异的来源，可能会对故意的分支错误预测造成严重损害。尽管静态分析可以定性地验证推测执行下的无时序泄漏特性，但它不能产生包括输入和推测流的背书以深入诊断泄漏。这项工作提出了一个新的符号执行为基础的方法，SpecuSym，精确检测缓存定时泄漏引入推测执行。给定一个程序（在非推测性执行中无泄漏），SpecuSymsystematically探索程序状态空间，在条件分支处对推测性行为进行建模，并随着后续路径探索积累缓存副作用。在动态执行过程中，SpecuSym根据指定的缓存模型构造内存访问的泄漏谓词，并进行基于约束求解的缓存行为分析，以检查新的缓存行为。我们已经实现了SpecuSymatop KLEE，并根据15个开源基准对其进行了评估。实验结果表明，SpecuSym在3种不同的缓存设置下成功地检测到6个程序中2 ~ 61个漏洞，并在最近的工作中发现了2个程序中的误报。
2020-02-14 cs.CR cs.SE
Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics
本文利用形式化ISA语义实现二进制代码的精确符号执行，构建了可扩展的RISC-V原型，并通过实验发现angr中的五个未知缺陷。
2025-01-20 cs.CR cs.PL cs.SE
Dynamic Symbolic Execution for Semantic Difference Analysis of Component and Connector Architectures
RWTH Aachen University（亚琛工业大学）；Software Engineering, RWTH Aachen University（软件工程，亚琛工业大学）
本文提出利用动态符号执行分析组件和连接器架构的语义差异，通过收集运行时数据识别关键执行轨迹，但指出可扩展性是主要限制。
2026-03-07 cs.FL cs.SC cs.SE
