自二十世纪以来,计算机技术作为高新科技行业的代表,被应用到人类社会生产生活的各个环节,在许许多多重要的领域发挥着不可替代的关键作用。进入二十一世纪以来,计算机技术更是进入了飞速发展的时代。无论是工业生产还是社会经济,都受到计算机技术迅猛发展的带动,计算机技术正以不可思议的速度和力度改变着人类社会活动。但同时,计算机软件的安全问题也对社会经济和生产活动造成了严重的影响。研究发展软件测试技术是保障软件可靠运行的重点。在软件测试的研究过程中,人们提出了多种测试技术。从依靠人工的静态检测技术,到自动化执行的模糊测试技术,软件测试技术伴随着现代软件规模的提高和安全需求的上升,一直不断发展。随着现代软件规模的加大,复杂度不断增加,对软件安全性的需求也不断上升,传统的测试技术因自身的局限已无法满足当前的软件安全性的需求。而动态符号执行技术因自身具有的优异特性在软件测试领域中受到了广泛的关注。动态符号执行技术基于二十世纪七十年代提出的符号执行技术之上,具有自动化测试用例生成,程序路径覆盖率高,无需人工操作等优点,受到了当前众多高校和科技公司的关注,许多动态符号执行工具不断出现,并在实际应用中取得了很好的成绩。但是动态符号执行技术还存在着一些需要解决的关键问题如路径爆炸,指针计算以及约束求解等问题。其中,约束求解的性能直接关系到动态符号执行的运行效率,成为了制约动态符号执行技术发展的主要障碍。本论文着眼于KLEE的约束求解技术,在KLEE的约束求解模块内设计出多约束求解器并行化运行的结构,将微软公司研究设计的性能出色的Z3求解器移植到KLEE工具中。使其与KLEE中原有的STP求解器并行工作,达到提高KLEE约束求解效率的目的。为验证多求解器并行化对KLEE约束求解性能的提升效果,本文选取了Unix Coreutils程序组件中的9个程序作为实验用例分别测试应用STP求解器和应用Z3求解器的KLEE工具对这9个程序的测试效果。通过测试数据,比较出本文所提出的多求解器并行化设计在KLEE中的有效性:与原KLEE的约束求解器相比,本文提出的设计可有效的改进KLEE的约束求解性能,提高了KLEE的执行效率。