Concolic Testing in CLP
Concolic测试是一种基于具体执行和符号执行相结合的流行软件验证技术。它的主要重点是发现bug和生成测试用例，目的是最大限度地提高代码覆盖率。以前的逻辑编程中的concolic测试方法是不健全的，因为它只处理正约束（通过替换），但不能表示负约束。在本文中，我们提出了一个新的框架concolic测试的CLP程序，概括了以前的技术。在CLP设置中，可以以自然的方式表示正约束和负约束，从而产生一种合理且（潜在地）更有效的技术。定义验证和测试技术CLP程序越来越相关，因为这个框架正在成为流行的中间表示，以分析在其他编程范式编写的程序。
2020-08-05 cs.LO cs.PL cs.SE
Towards Concolic Testing for Hybrid Systems
混合系统表现出连续和离散的行为。众所周知，分析混合动力系统是很困难的。受concolic测试（程序）的想法的启发，我们研究是否可以结合随机抽样和符号执行，以有效地验证混合系统。我们确定了一个充分条件下，这样的组合比随机抽样更有效。此外，我们分析了不同的策略相结合的随机抽样和符号执行，并提出了一个算法，它允许我们动态切换它们之间，以降低整体成本。我们的方法已被实现为一个基于Web的检查器名为Hypogram。为了测试其有效性，已经用基准混合动力系统和水处理系统对Hyphase进行了评估。
2016-08-31 cs.LO cs.SE
Quantum Concolic Testing
本文提出首个面向量子程序的 concolic 测试框架，通过量子约束生成与符号化方法生成路径约束并引导探索，有效提升分支覆盖率与 bug 检测能力。
2025-06-01 cs.SE quant-ph
Cottontail: Large Language Model-Driven Concolic Execution for Highly Structured Test Input Generation
本文提出LLM驱动的共模执行引擎Cottontail，通过ESCT路径表示、LLM约束求解器和历史引导种子获取，解决结构化测试输入生成问题，显著提升覆盖率并发现6个新漏洞。
2025-10-14 cs.SE
Prioritising Server Side Reachability via Inter-process Concolic Testing
内容：大多数自动化白盒测试的方法都将Web应用程序的客户端和服务器端相互隔离。这样的测试人员缺乏对被测Web应用程序的整体程序视角。询价：我们假设，一个额外的整个程序的角度将使测试人员发现哪些服务器端的错误可以触发一个实际的最终用户通过客户端访问应用程序，哪些只能在假设的情况下触发。方法：在本文中，我们探讨了在测试中采用这种全程序视角的想法。为此，我们开发了一种新颖的concolic测试器，它在全栈JavaScript Web应用程序上运行，其中客户端和服务器端都是通过异步消息进行通信的JavaScript进程-由WebSocket或Socket. IO库启用。知识：我们发现，整个程序的角度来看，能够辨别高优先级的错误，这是从一个特定的客户端，从低优先级的错误，这是不能通过测试的客户端访问。透视图的另一个好处是，它允许自动化测试人员从最终用户的角度构造实际的、逐步的场景来触发服务器端错误。基础：我们应用于一组Web应用程序，以评估测试在区分高优先级和低优先级错误方面的有效性。结果表明，正确分类的大多数服务器错误。重要性：本文展示了测试作为自动测试Web应用程序的新方法的可行性。将错误分类为高或低重要性有助于开发人员对用户可能遇到的错误进行优先级排序，并推迟对不太容易达到的错误的诊断。
2021-03-04 cs.SE
GreyConE: Greybox fuzzing+Concolic execution guided test generation for high level design
由于复杂的分支条件、循环结构和硬件设计固有的并发性，对高级设计进行详尽的测试是一个艰巨的挑战。测试工程师的目标是生成满足各种代码覆盖率指标的高质量测试用例，以确保设计中出现的错误最少。在测试SystemC设计之前的工作是时间效率低下的，这阻碍了在较短的时间跨度内实现所需的覆盖。我们交错灰盒模糊和concolic执行系统的方式，并生成质量测试用例加速测试覆盖率指标。我们的结果优于国家的最先进的方法在测试用例的数量和分支覆盖的一些基准，和运行时间为他们中的大多数。
2022-07-13 cs.CR cs.SE
Dynamic Symbolic Execution of Higher-Order Functions
concolic测试的有效性随着程序规模的增加而恶化。一个有希望的方法是模块化地测试程序，例如，在每个函数或类的基础上。唉，这种想法在现代程序设计语言中遇到了障碍。在现代语言中，组件需要函数、对象甚至类作为输入。问题的关键是，现有的concolic测试技术不能忠实地捕捉一个高阶程序和它的输入之间的复杂的相互作用，以提取它在一阶公式，SMT求解器可以工作。在本文中，我们采取的第一步解决问题，我们提供了一个设计，语义和原型concolic测试高阶函数。受高阶符号执行工作的启发，我们的模型构造了具有规范形状的高阶函数的输入。这使得concolic测试器能够跟踪高阶函数的控制流路径的哪些部分取决于其输入的形状，哪些部分不取决于其输入的形状。concolic测试器将不依赖于输入形状的部分编码为一阶公式。随后，类似于一阶concolic测试器，它利用SMT求解器产生另一个具有相同形状的输入，但探索高阶函数的不同控制流路径。作为一个单独的维度，concolic测试器迭代地探索输入的规范形状，并调查高阶函数与其输入交互的所有方式，搜索bug。为了验证我们的设计，我们证明，如果一个高阶函数有一个错误，我们的concolic测试最终将构建一个输入，触发错误。使用我们的设计作为蓝图，我们实现了一个原型concolic测试仪，并确认它发现了各种高阶程序从文献中的错误。
2020-06-20 cs.PL cs.SE
SAVIOR: Towards Bug-Driven Hybrid Testing
混合测试结合了模糊测试和concolic执行。它利用模糊测试来测试容易到达的代码区域，并使用concolic执行来探索由复杂分支条件保护的代码块。然而，其以代码覆盖为中心的设计在漏洞检测方面效率低下。首先，它盲目地选择concolic执行的种子，旨在不断探索新代码。然而，正如统计数据所显示的那样，所探索的代码的很大一部分通常是没有bug的。因此，在混合测试中对代码的每一部分给予同等的关注是一种非最优策略。它将真正漏洞的检测速度降低了43%以上。第二，传统的混合测试在到达一段代码后快速前进，而不是检查内部隐藏的缺陷。它可能经常错过微妙的漏洞，尽管它已经探索了易受攻击的代码路径。我们提出了SAVIOR，一个新的混合测试框架开创了错误驱动的原则。与现有的混合测试工具不同，SAVIOR优先考虑可能发现更多漏洞的种子的concolic执行。此外，SAVIOR还验证了程序执行路径上所有的漏洞位置，并通过SMT约束对故障情况进行建模，对漏洞的可行性进行推理，生成具体的测试用例作为证明。我们的评估表明，错误驱动的方法优于主流的自动化测试技术，包括最先进的混合测试系统驱动的代码覆盖率。平均而言，SAVIOR比DRILLER和QSYM分别快43.4%和44.3%，分别多发现了88个和76个独特的漏洞。根据对11个模糊基准测试程序的评估，在前24小时内，SAVIOR触发了481个UBSAN违规，其中24…
2019-06-18 cs.SE
Exposing Go's Hidden Bugs: A Novel Concolic Framework
Telecom Paris（巴黎电信学院）；Ledger Donjon
本文提出Zorya框架，结合具体和符号执行技术全面评估Go程序，通过系统探索执行路径发现传统测试无法检测的漏洞，并利用Ghidra的P-Code中间表示进行分析。
2025-05-26 cs.CR cs.SE
Coyote C++: An Industrial-Strength Fully Automated Unit Testing Tool
本文介绍了Coyote C++，一款基于混合符号执行的工业级C和C++全自动化单元测试工具，它无需用户参与即可一键完成测试生成与执行，持续达到约90%的代码覆盖率。
2023-10-23 cs.PL cs.SE
CUTECat: Concolic Execution for Computational Law
CUTECat利用合流执行结合默认逻辑，针对计算法实现生成测试用例，覆盖所有分支，提升法律程序正确性，推动形式化方法在立法中的应用。
2025-01-23 cs.PL cs.SE
ColorGo: Directed Concolic Execution
本文提出ColorGo，一种结合编译式符号执行与增量着色的定向白盒模糊测试器，在保持高精确性的同时实现高可扩展性，在真实程序上比AFLGo快达100倍。
2025-05-27 cs.CR cs.SE
Failure-Guided Fuzzing for Hybrid Quantum-Classical Programs
University of Maryland, Baltimore County（马里兰大学巴尔的摩县分校）
本文研究了混合量子-经典程序的基于失败的模糊测试，通过两阶段策略发现非收敛种子并局部模糊量子电路参数，实验表明利用失败信息能提升测试效果，但协同种子发现的效果依赖于工作负载。
2026-05-14 cs.SE quant-ph
Fuzzing Symbolic Expressions
近年来，软件测试取得了广泛的成果，探索了不同的方法和方法，从模糊器到符号引擎，以及介于两者之间的各种实例，如concolic执行和混合模糊。其中许多工具的一个关键组成部分是可满足性模理论（SMT）求解器，用于对分析期间收集的符号表达式进行推理。在本文中，我们研究是否可以借用模糊域的技术来检查是否符号公式是可满足的concolic和混合模糊引擎的背景下，提供了一个可行的替代经典SMT解决技术。我们设计了一个新的近似求解器，FUZZY-SAT，并表明它是竞争和互补的最先进的求解器，如Z3处理混合模糊器产生的查询。
2021-02-12 cs.CR cs.SE
A Feature-Oriented Corpus for Understanding, Evaluating and Improving Fuzz Testing
Fuzzing是一种很有前途的安全漏洞检测技术。新开发的模糊器通常根据在易受攻击的程序/二进制文件上发现的错误数量进行评估。然而，现有的语料库通常不捕捉的功能，防止模糊发现错误，导致模糊的利弊评价的结论。一个典型的例子是，Driller比AFL检测到更多的错误，但它的评估无法确定Driller的进步是否源于concolic执行，因为，例如，它在解决数据集的魔法值方面的能力尚不清楚。在本文中，我们提出了解决上述问题的基础上产生语料库的搜索阻碍功能。作为概念验证，我们设计了FEData，这是一个原型语料库，目前专注于四个搜索阻碍功能，以生成用于模糊测试的易受攻击程序。与现有的只能回答“如何”的语料库不同，FEData还可以通过暴露（或理解）模糊器中已识别弱点的原因来进一步回答“为什么”。“为什么”信息是改进模糊器的关键。
2019-05-04 cs.SE
Taming the Beast: Fully Automated Unit Testing with Coyote C++
本文提出 Coyote C++，一个面向 C 和 C++ 的全自动化白盒单元测试工具，结合 concolic 执行引擎与自动化测试套件生成，实现高覆盖率与高速测试，并支持手动优化，使 C++ 自动化测试在工业应用中真正可行。
2024-01-04 cs.PL cs.SE
Constraint-based Adversarial Example Synthesis
本研究扩展了Concolic Testing工具PyCT以支持更广泛的神经网络操作，通过系统生成预测路径约束来识别潜在对抗样本，揭示了Python神经网络模型的脆弱性并强调了稳健测试方法的重要性。
2024-06-03 cs.CR cs.SE
Detecting Buggy Contracts via Smart Testing
Columbia University（哥伦比亚大学）；The University of Chicago（芝加哥大学）
针对混合动态分析难发现智能合约深层缺陷的问题，本文提出可自主决策的 SmartSys，利用基础模型选择分析技术、生成模糊目标并结合动态反馈抑制幻觉，发现长期遗漏漏洞并提升覆盖率。
2024-09-06 cs.LG cs.PL cs.SE
PALM: Synergizing Program Analysis and LLMs to Enhance Rust Unit Test Coverage
State Key Laboratory for Novel Software Technology, Nanjing University（南京大学软件新技术国家重点实验室）；Software Engineering Application Technology Lab, Huawei（华为软件工程应用技术研发实验室）
本文提出PALM框架，通过程序分析提取分支条件与路径约束并构造LLM提示，自动生成Rust高覆盖率单元测试，在15个开源crates上达到接近人工的覆盖率且多数提交被接受。
2025-09-29 cs.SE
