形式验证的方法主要有模型检测和演绎推理两种。模型检测的优点是验证过程是自动的，缺点是具有状态爆炸问题，不利于处理大型系统。演绎推理具有可以处理无穷状态系统的优点，但验证过程不是完全自动的且对用户的数学知识要求较高。有穷自动机、下推自动机、petri网等迁移系统常常被用于系统建模，在这些系统中大部分系统分析问题可以规约到可达性问题。因此，可达性问题在形式验证中是非常重要的。交替式下推系统是形式化验证中的一种重要方法。下推系统的可达性问题传统的解决方法是通过在原本的下推系统之外构造一个新的有穷状态自动机，使得一个状态在下推系统中可达当且仅当这个状态能被新构造的有穷状态自动机所接收。本文采用另一种解决交替式下推系统可达性问题的方法，即利用逻辑推演解决这些问题，在原有的下推系统中做一个饱和的过程，使得一个状态是可达的当且仅当它在经过饱和后的下推系统中有一个具有切消去性质的证明，而省去了构造有穷状态自动机的过程。　　本文的第一个工作是研究与实现一个关于交替式下推系统中可达性的证明系统，该系统可以将无穷证明树转换为有穷树。首先通过读入文本格式的输入文件，解析输入文件并得到交替式下推系统;然后，将交替式下推系统转换成小步交替式下推系统，通过循环迭代的方式对系统进行饱和操作直至规则收敛，得到多元自动机;接下来利用全排列算法实现系统的完备化，得到完备化的多元自动机，并利用深度优先算法实现余归纳方式的搜索证明。　　本文的第二个工作是对生成的证明树在三维空间进行可视化。通过改进力导向布局算法中的斥力一引力模型，实现了树节点的自动布局;利用节点颜色的体现节点之间父子关系;通过增加旋转、缩放、高亮和事件响应功能，使用户更好的理解证明树。