有了程序的部分执行历史或轨迹如何通过形式化验证来判断这些轨迹的正确性？

通过形式化验证可以使用数学方法来证明程序的正确性，其中包括以下步骤：

1. 建立模型：根据程序的执行轨迹，建立一个数学模型。这个模型可以是有限状态机、Petri网等。

2. 定义性质：在建立好模型之后，需要定义要验证的性质。这些性质可以是安全性、一致性、死锁等。

3. 验证方法：根据定义的性质，使用不同的验证方法进行验证。常用的方法有模型检测、定理证明等。

4. 分析结果：如果验证结果显示程序满足要求，则程序可以被认为是正确的。如果验证结果显示程序存在错误，则需要进行修复。

形式化验证可以帮助开发人员在程序设计和实现的早期阶段发现问题，减少后期修复成本，提高程序的可靠性和安全性。