程序调试是软件开发过程中最关键的环节之一，调试的开销将直接影响到软件的成本和软件公司的收益。对于程序员来说，调试也是一个非常单调乏味的工作。因此，程序的自动化调试方法成为了计算机领域的热点课题，得到不同领域众多研究者的关注，继而出现了各种各样的自动化调试方法，如算法调试、切片技术、基于模型调试、基于概率调试、基于程序状态调试、Delta调试等等。　　 现有的大多数调试技术都是经验性的，即依靠专家经验和一些启发式性质。为此，刘咏梅教授分析了要基于第一原理为程序调试建立一个精确的理论基础的重要性。本文研究的起点是张翔宇教授等人提出的一种程序调试的单谓词开关方法，其主要思想是通过改变程序运行过程中的一个谓词实例的取值使得原来错误的程序最终运行得到正确的结果，然后根据被开关的谓词利用切片技术来确定诊断范围。但很多情况下，只对单个谓词实例进行开关并不能够使程序得到正确的运行。针对单谓词开关算法的局限性，本文提出有界调试的多谓词开关算法(bounded debugging via multiple predicate switchingalgorithm，BMPS)，通过在程序运行过程中开关多个谓词实例来得到一个正确的运行，且在此运行中每个循环的执行次数不超过一个给定的上界。BMPS算法可以通过一个可满足性(satisfiability，SAT)求解器来实现。　　 文中讨论的程序错误主要为右端(righthandside，RHS)错误，即错误出现在控制谓词或者赋值语句的右边。对于只含条件控制语句的程序，本文证明了BMPS算法对于RHS错误是准完备的，即真实错误的部分语句一定会被BMPS算法返回。对于含循环的程序，本文证明了当循环展开的次数足够大时，BMPS算法对于RHS错误是准完备的。　　 本文对所提BMPS算法进行了初步的实验评估。本文深入分析了调试领域权威标准西门子标准中的TCAS程序，得出TCAS程序的41个错误版本中有39个版本是RHS错误。本文还对大量小型错误C程序进行了调试实验，实验结果表明BMPS能够有效地锁定错误。