终止性验证可从正向和反向两个方向进行。正向验证终止性是从正向的角度寻找证据，证明被验证对象不存在状态无限循环、无法终止的状况；反向验证终止性是从方向的角度，寻找一条无穷循环的路径或者方法，从而证明被验证对象不终止。被验证对象可以是软件、需求，也可以是规约和设计等个体。被验证对象的终止性分为可终止和不可终止。如果被验证对象经过一系列变迁，最终能够达到预期状态，那么该验证对象是可终止的，否则就是不可终止的。

终止性验证可采用传统验证方法进行，也可采用形式化验证方法进行。传统验证方法包括测试和模拟，但这种方法受限于测试用例或模拟样本的可穷性，不能覆盖所有情况，所得到的结果在准确性和可靠性上有欠缺。形式化验证方法是从数学上完备地证明被验证对象是否实现了预期功能或者达到预期状态的一种方法，其验证结果是根据严密的数理逻辑推导而出，所以得到的结果具有准确性和完备性。形式化验证方法是对传统验证方法的一种重要补充，且更为客观、科学。

在实现形式化的终止性验证时，首先需要对被验证对象的终止性进行详细定义，明确该对象在什么情况下可称之为可终止或不可终止。然后，对各种情况加以综合分析，确定该对象的可终止性判定规则。之后，根据判定规则来设计并实现可终止性判定算法，最终完成针对被验证对象的终止性验证。终止性验证注重的是被验证对象的整体属性，是保证其正确性的基础，因此终止性验证是计算机验证技术中不可或缺的组成部分。