Pegasus：声音连续不变生成
Pegasus: Sound Continuous Invariant Generation
摘要：
连续不变量是混合和连续系统演绎验证的重要组成部分。就像离散不变量被用来推理离散系统的正确性而不必展开它们的循环一样，连续不变量被用来推理微分方程而不必求解它们。连续不变量的自动生成仍然是混合系统安全性形式证明自动化的最大实际挑战之一。目前有许多不同的方法可用于生成连续不变量;然而，这些丰富的不同技术带来了许多挑战，不同的方法具有不同的优点和缺点。为了解决其中的一些挑战，我们开发了Pegasus：一个自动连续不变发生器，允许各种方法的组合，并将其与混合系统的KeYmaera X定理证明器相结合。我们描述了这种集成的一些架构方面，评论其方法和挑战，并提出了一套基准测试的实验评估。
英文摘要：
Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
