SHF: CSR: Small: Bounded Verification and Bounded Synthesis

许多现代人类工程系统的一个共同特征是，它们涉及离散的软件系统和连续的物理系统之间的交互作用，例如医疗设备、汽车和航空航天飞行器。有几个这样的系统是安全关键的，故障可能是灾难性的。如何保证这些系统的设计和建造是正确的？基于测试的传统方法需要补充基于正式方法的方法。不幸的是，形式核查总体上是一个棘手的问题，因此，没有一种单一的形式核查方法可以统一地很好地执行。该项目开发了一种新的正式核查方法，补充了现有的方法。拥有一套正式的验证工具可以帮助在设计周期的早期发现错误，以降低总体开发成本，并增加对所设计的复杂网络物理系统的保证。该项目通过开发一种新的形式验证方法，称为有界验证，为现有的形式验证技术做出了贡献。有界验证通过对将建立属性的证人执行有界搜索来验证系统。根据不同的性质，证人可以是Lyapunov函数、归纳不变量、控制不变量等。对证人的搜索被转换为量化(\EXISTS\FORALL)公式的可满足性。可满足性是使用包括反例引导的归纳推理、成分推理、模拟和定点计算在内的技术组合来确定的。设计的有界验证生成的证明人被用来引导实现的形式验证。该项目还扩展了有界验证方法，以执行系统的自动综合。有界验证明确地为正确性提供了见证，这可以用来帮助认证过程。该项目还为定理证明领域和正式验证领域之间的互动引入了新的联系，旨在促进这两个领域的合作和促进进展。

A common feature of many modern human-engineered systems, such as medical devices, automobiles and aerospace vehicles, is that they involve interaction between discrete software systems and continuous physical systems. Several such systems are safety critical and failures can be catastrophic. How to guarantee that these systems are designed and built correctly? Traditional approaches based on testing need to be supplemented with approaches based on formal methods. Unfortunately, formal verification is an intractable problem in general and, hence, no single formal verification approach can uniformly perform well. This project develops a new approach for formal verification that complements existing approaches. Having a suite of formal verification tools can help find errors earlier in the design cycle to reduce overall development cost and increase assurance of designed complex cyber-physical systems. This project contributes to the existing formal verification technology by developing a new approach for formal verification, called bounded verification. Bounded verification verifies a system by performing a bounded search for a witness that would establish the property. Depending on the property, a witness is a Lyapunov function, an inductive invariant, a controlled invariant and so on. Search for a witness is cast as satisfiability of a quantified (\exists\forall) formula. Satisfiability is decided using a combination of techniques including counterexample guided inductive reasoning, compositional reasoning, simulations, and fixpoint computations. Witnesses generated by bounded verification of the design are used to bootstrap formal verification of the implementation. This project also extends the bounded verification approach to performing automated synthesis of systems. Bounded verification explicitly provides witnesses for correctness, which can be used to aid in the certification process. This project also introduces new links for interaction between the fields of theorem proving and formal verification that aim to foster collaboration and promote progress in both areas.