Verified Model Checkers

模型检验是硬件和软件系统验证即可靠性保证的最重要的实际应用方法。这个项目的目标是(i)开发两个模型检查器，每个都有不同的用途，以及（ii）使用交互式定理证明器证明它们的正确性，从而显著提高模型检查本身的可靠性。除了整体模型检查器之外，我们还将验证其本身有用的基本组件，例如，等效检查器和无限单词自动机的确定方法。开发第一个模型检查器的主要目标是高性能。它应该与知名的（未经验证的）SPIN模型检查器竞争。这需要高效的算法，而这些算法很难验证。这里的主要焦点在于验证命令式和空间高效的数据结构。第二个模型检查器针对更广泛的模型类别，这些模型可能显示概率行为，并且其属性只能以一定的概率保证。对于概率模型检查，我们的重点是结合验证图，自动机和数值算法。这里，我们要验证线性方程和线性规划的解。我们希望利用已经存在的未经验证的求解器，这些求解器已经优化了很长时间。因此，我们将开发验证工具，以证明此类求解器的输出通常是近似的，对于给定的容错是正确的。这是可能的，由于各自的线性方程和程序的特定性质。

Model Checking is the most important practically applied method for verification, i.e., reliability assurance, of hardware and software systems. The goal of this project is to (i) develop two model checkers, each with distinct use, and (ii) prove their correctness using an interactive theorem prover, thus significantly increasing the reliability of model checking itself. Apart from the monolithic model checkers, we will also verify fundamental components that are useful on their own, for instance, equivalence checkers and determinization methods for automata on infinite words.The main aim of developing the first model checker is high performance. It shall be competitive with the well-known (unverified) SPIN model checker. This requires efficient algorithms, which are challenging to verify. The main focus here lies on verifying imperative and space-efficient data structures.The second model checker is targeted at a wider class of models, that may show probabilistic behavior and whose properties can only be guaranteed with certain probability. For probabilistic model checking, our focus is on combining verified graph, automata, and numerical algorithms. Here, we want to verify solvers for linear equations and linear programs. We want to exploit already existing unverified solvers, which have been optimized for a long time. Therefore, we will develop verified tools to certify that the output of such solvers, which is usually approximate, is correct for a given error tolerance. This is only possible due to specific properties of the respective linear equations and programs.