混合系统的KeYmaera X定理证明 自动驾驶汽车,自动驾驶机器人,现代飞机或机器人手术:我们越来越多地将生命委托给计算机,因此,除了最高的安全标准-数学正确性证明之外,我们应该一劳永逸。 可以使用KeYmaera X证明程序来构造此类网络物理系统的证明。 作为混合系统定理的证明者,KeYmaera X用微分动态逻辑分析了控制程序和受控系统的物理行为。 KeYmaera X具有仅约2000行代码的最小内核,该内核隔离了所有对可靠性要求严格的推理。 如此小的和简单的证明者核心使信任验证结果变得更加容易。 基于核心驱动器的自动预定义搜索的预定义和自定义策略。 KeYmaera X带有一个基于W