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.