Verified Model Checkers

点击翻译按钮获取中文摘要

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.