软件质量问题是工业界和学术界共同关注的热点问题.软件测试是软件生产质量保障中的一项重要技术，它的主要目的是尽可能地减少程序的错误.本文着重研究了如何将约束求解应用到自动化软件测试.这些研究大致可以分为如下三个方面.　　 本文第一方面的工作是关于白盒测试的研究.白盒测试是面向程序代码的精确测试方法.我们可以采用符号执行的方法来处理程序中的路径，进而测试程序某些方面的性质.然而，由于符号执行的代价比较高，测试程序的所有路径几乎不可能；同时由于不可行路径的影响，我们需要采用一些合适的测试准则或者路径选择策略来指导我们生成测试路径集合.这一方面的工作包括两个部分.　　 1)本文提出了一种有效地产生可行基本路径的自动化方法，能在可接受的时间内针对真实C单元程序生成可行的基本路径.这种方法产生的基本路径集合的带权路径长度的总和是最小的.2)BPEL是一种业务流程描述语言，它可以表达程序复杂的并发行为.本文提出了一种新颖的基于并发路径分析的BPEL测试生成方法.我们采用了一些限制组合的技术以及路径覆盖准则来避免测试路径的组合爆炸.这个框架是模块化的，所以很多测试中采用的技术，比如不同的测试准则和约束处理技术，可以应用到其中.　　 本文第二方面的工作属于黑盒测试.黑盒测试用于对程序的功能和接口进行测试.我们可以用约束描述被测系统的规约或者测试准则，在这种情况下，黑盒测试用例的生成问题可以转化为有限约束满足问题.这一部分的工作也包含两部分.1)提出了基于SAT和回溯搜索算法的方法来解决组合测试生成问题.并提出了一个新颖的剪枝策略SCEH，用于提高算法的效率.一些已有的启发式搜索策略，以及一些对称打破技术，也被应用到我们的回溯搜索算法中.实验结果表明，我们的方法在一些小规模实例上的表现优于其它的方法.2)对于针对布尔规范的MUMCUT测试准则，本文提出了一种基于SAT的自动测试生成方法.为了提高采用完备性SAT工具时的求解效率，我们采用了一些对称打破技术.　　 本文第三方面的工作是分析线性数值约束的逻辑关系.在程序分析和验证中，相同的约束可能会需要反复处理.一种可能的加速方法就是预先找到约束之间的逻辑关系.这种关系可以用规则来描述.我们不大可能在多项式时间内找到所有的规则.本文提出了一种基于搜索的算法，以及一些启发式策略，用于寻找这些规则.实验结果表明我们的方法能够在可接受的时问内产生足够的规则.