软件质量保障是计算机科学中的重要研究问题。在航空、航天、国防、医疗等安全攸关的领域,软件的质量保障尤为重要。符号执行是于上世纪70年代提出的一种基本的程序分析技术,可以被用于生成测试用例、查找程序缺陷、证明程序的性质等,进而提高软件的质量。符号执行使用符号值代替程序的输入值以符号化地执行程序,并使用约束求解器来判定路径的可行性。符号执行技术能够遍历程序的路径空间,以达到对程序的透彻理解。近年来,由于相关算法的进展、约束求解技术的发展以及机器速度的提升,符号执行技术重新成为了研究热点,并得到了学术界和工业界的广泛关注。然而,在分析大规模程序或者较复杂的程序时,符号执行在可扩展性、可行性等方面仍然面临着一些挑战。其中路径爆炸以及约束求解开销是影响符号执行可扩展性的主要因素,而实际应用领域的复杂性则大大影响了符号执行方法的可行性。本文围绕符号执行方法的可扩展性及可行性展开了一系列研究,旨在进一步推动符号执行方法在软件测试、分析及验证中的应用。本文的主要贡献包括:1)提出了猜测符号执行方法。猜测符号执行将现代处理器流水线结构中的猜测思想引入到符号执行中,在遇到分支语句时不一定调用约束求解器,而是预先对后续的语句进行符号执行。仅当路径上未判定的分支语句个数达到一定的数量或者到达路径末端时,才对路径的可行性进行判定。如果猜测成功,则能有效减少约束求解器的调用次数;如果猜测失败,则使用一套高效的回溯机制将系统状态回滚到最后一个可行的分支点处。本文对该方法的效果进行了理论分析,并进一步提出了三种优化方法,从不同的侧面进一步提升猜测符号执行的效果。实验结果显示,猜测符号执行能够平均减少38.5%的约束求解器的调用次数以及28.5%的搜索时间。2)提出了正规性质制导的动态符号执行方法。符号执行作为一种路径敏感的程序分析方法,可以很自然地用以检查程序正规性质。然而,符号执行技术受限于路径爆炸问题。本文提出了正规性质制导的动态符号执行方法。该方法基于如下的规律:在程序路径空间中,包含有特定的事件序列的路径才满足正规性质。该方法使用动态符号执行技术搜索程序的路径空间,其关键在于能够根据待探索分支的历史行为和未来行为对其进行评估,优先探索那些最有可能指向满足正规性质的路径的待探索分支。在该方法中,待探索分支的历史行为和未来行为均被表示为有限状态自动机的状态集合。我们使用调用上下文敏感、流敏感的过程间数据流分析来计算分支的未来行为。该方法结合了静态分析、动态符号执行以及运行时验证三个领域的技术,使不同的技术相互支持和补充,具有高效、无误报等优点。本文还提出了一种针对限界的调用上下文敏感的数据流分析的优化方法,能够以极小的代价提高分析精度。实验显示,该方法将动态符号执行检查程序正规性质的效率提高至少1至2个数量级。3)基于符号执行的Web服务测试方法。面向服务的应用本身的分布性、松耦合性、动态性等特征为服务测试带来了诸多困难,也使得符号执行方法无法直接应用于服务测试。本文针对服务测试领域中符号执行方法的可行性问题,给出了协作式Web服务测试框架,填补了符号执行方法和服务应用之间的鸿沟,使得符号执行方法能够应用于服务测试。该框架基于如下三个基本思想:一、使用“伴随服务”使服务测试白盒化,并避免测试对服务正常运行的干扰;二、将符号执行工具服务化,使框架能够根据测试需求自动地匹配符号执行工具,辅助服务测试的自动化;三、使用测试中介使服务测试流程自动化,以适应服务计算中在线测试的需求。该框架提供了一系列机制,使得符号执行工具能够自动化地应用于服务测试。本文介绍了该框架的设计与实现细节,并通过实验展示了该框架的通用性与可扩展性。