符号测试

符号测试（具体和符号的谐音）是一种混合的软件验证技术，沿着具体执行（对特定输入进行测试）的路径执行符号执行，这是一种将程序变量视为符号变量的经典技术。符号执行与自动定理检验器或基于约束逻辑编程的约束解算器结合使用，生成新的具体输入（测试用例），目的是xxx限度地提高代码覆盖率。它的主要重点是在现实世界的软件中寻找错误，而不是证明程序的正确性。这些工具（DART和CUTE，EXE）将协同学测试应用于C程序的单元测试，协同学测试最初被认为是对既定随机测试方法的白盒改进。该技术后来被推广到用jCUTE测试多线程的Java程序，并从其可执行代码（工具OSMOSE）进行单元测试。它还与模糊测试相结合，并由微软研究院的SAGE扩展到检测大规模x86二进制文件中可利用的安全问题。协同学的方法也适用于模型检查。在协程模型检查器中，模型检查器遍历了代表被检查软件的模型状态，同时存储了具体状态和符号状态。符号状态用于检查软件的属性，而具体状态则用于避免到达不可到达的状态。

传统的基于符号执行的测试的实施需要为编程语言实现一个完整的符号解释器。协和测试的实施者注意到，如果符号执行可以通过仪器化与程序的正常执行相结合，就可以避免全面的符号执行的实施。这种简化符号执行的想法催生了协约测试。

自2005年引入协同学测试以来的十年间，协同学测试（以及更普遍的基于符号执行的程序分析）的兴起的一个重要原因是SMT求解器的效率和表达能力有了极大的提高。导致SMT求解器快速发展的关键技术发展包括理论的组合、懒人求解、DPLL(T)和SAT求解器速度的巨大改善。