Computergestützte Verifikation von Automatenkonstruktionen für Model Checking

模型检验是一种实用的对硬件和软件系统进行验证和证伪的方法，zur Sicherstellung der Zuverlässigkeit dieser Systeme.在这个项目中，模型检测的核心算法的实现是非常重要的，它与一个交互式的理论解释者一起工作，所以模型检测的工作是非常重要的。我们将致力于自动理论分析模型检验。因此，模型检测的验证方法也是自动化理论的形式化，它不仅仅是一个简单的基础，而是一个理论中的一个重要研究，它对信息学的研究是如此的重要。该项目是一个世界上最好的，在韦尔登中同时进行理论和程序的信息化实践的理论和实施。Herausragende Ergebnisse waren bisher z.B.一个验证者C-Bracker和一个验证者Betriebssystemkern。我们将在这个形式化解决方案的中心研究模型检测和自动化理论。

Model Checking ist die in der Praxis wichtigste Methode zur Verifikation und Falsifikation von Hardware- und Softwaresystemen, d.h., zur Sicherstellung der Zuverlässigkeit dieser Systeme. Ziel des Projekts ist es, Implementierungen von Kernalgorithmen des Model Checking bereitzustellen, die mit Hilfe eines interaktiven Theorembeweisers als korrekt nachgewiesen wurden, um so die Zuverlässigkeit des Model Checking selbst signifikant zu erhöhen. Wir konzentrieren uns auf den sehr weit entwickelten automatentheoretischen Ansatz zum Model Checking. Daher sind sowohl die Verifikation wichtiger Algorithmen des Model Checking als auch die Formalisierung der Automatentheorie das Ziel — letzteres nicht nur als notwendige Basis, sondern als langfristige Investition in eine Theorie, die für die Informatik so grundlegend wie keine andere ist. Dieses Projekt ist Teil einer wachsenden weltweiten Bestrebung, die Trennung zwischen Theorie und implementierter Praxis der Informatik zu überwinden, indem Theorie und Programme simultan in einem Theorembeweiser formalisiert werden. Herausragende Ergebnisse waren bisher z.B. ein verifizierter C-Compiler und ein verifizierter Betriebssystemkern. Wir wollen erstmalig das Model Checking und die Automatentheorie in das Zentrum eines solchen Formalisierungsprojekts stellen.