Correct by construction model checking

计算系统在日常生活中已经无处不在。这些系统的故障往往会导致大规模的中断，并产生巨大的成本。数学，特别是数学逻辑，在形式验证领域提供了重要的工具，其目的是确保计算系统的正确性。抽象数学模型用于提供系统的形式化表示，并用逻辑语言表达系统属性，以便可以验证这些属性是否适用于所考虑的系统。在抽象模型上验证给定属性的过程称为模型检查。虽然模型检查技术来源于数学思想，但在基础数学和实际验证算法之间往往存在令人担忧的差距。实现通常是特别的，用编程语言编写，只提供有限的支持来确保正确性。因此，无法保证验证软件本身工作正常。该项目的中心目标是通过开发数学技术来缩小这一差距，该技术允许从结构中提取正确的算法：通过从可以满足规范的证明中提取算法，它可以保证满足规范。通过将我们的工作建立在范畴论和协代数的丰富数学框架上并进行扩展，我们还将确保我们的模型检查算法能够验证不同类型的系统，并具有涉及成本、资源和概率的各种验证关注点。

Computational systems have become ubiquitous in everyday life. Failure of those systems often leads to large-scale disruptions and incurs huge costs. Mathematics and, in particular, mathematical logic provide important tools within the area of formal verification, which aims to ensure correctness of computational systems. Abstract mathematical models are used to provide formal representations of systems and system properties are expressed in a logical language, so that these properties can be verified to hold for the system under consideration. This process of verifying a given property on an abstract model is called model-checking.While the technique of model-checking is derived from mathematical ideas, there is often a worrying gap between the underlying mathematics and the actual verification algorithms. Implementations are often ad-hoc and written in programming languages that provide only limited support for ensuring correctness. Therefore, there are insufficient guarantees that the verification software itself is working correctly. The central goal of this project is to close this gap by developing mathematical techniques that allow the extraction of algorithms that are correct by construction: by extracting the algorithm from a proof that the specification can be fulfilled, it is guaranteed to fulfil it. By basing our work on and extending the rich mathematical framework of category theory and coalgebra, we will in addition ensure that our model-checking algorithms will be able to verify different types of systems with various verification concerns involving costs, resources and probabilities.