Computergestützte Verifikation von Automatenkonstruktionen für Model Checking

用于模型检查的机器设计的计算机辅助验证

• 批准号: 183790222
• 负责人: Professor Dr. Javier Esparza
• 金额: --
• 依托单位: Lehrstuhl Softwaretechnik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2010
• 资助国家: 德国
• 起止时间: 2009-12-31 至 2018-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/183790222?language=en
• 关键词: Computergest; tzte; Verifikation; von; Automatenkonstruktionen

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.

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

项目成果

Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm

经验证的 Gabow 强连通分量算法的高效实现

• DOI: 10.1007/978-3-319-08970-6_21
• 发表时间: 2014
• 期刊: Arch. Formal Proofs
• 作者: Peter Lammich

Büchi Automata Optimisations Formalised in Isabelle/HOL

Büchi 自动机优化在 Isabelle/HOL 中正式化

• DOI: 10.1007/978-3-662-45824-2_11
• 发表时间: 2015
• 作者: Alexander Schimpf;Jan-Georg Smaus
• 通讯作者: Jan-Georg Smaus

A Framework for Verifying Depth-First Search Algorithms

验证深度优先搜索算法的框架

• DOI: 10.1145/2676724.2693165
• 发表时间: 2015
• 期刊: Proceedings of the 2015 Conference on Certified Programs and Proofs
• 作者: Peter Lammich;René Neumann
• 通讯作者: René Neumann

From LTL to deterministic automata

从 LTL 到确定性自动机

• DOI: 10.1007/s10703-016-0259-2
• 发表时间: 2016
• 期刊: Formal Methods in System Design
• 影响因子: 0.8
• 作者: Javier Esparza;Jan Kretínský;Salomon Sickert
• 通讯作者: Salomon Sickert

Formal Verification of an Executable LTL Model Checker with Partial Order Reduction

• DOI: 10.1007/s10817-017-9418-4
• 发表时间: 2018-01-01
• 期刊: JOURNAL OF AUTOMATED REASONING
• 作者: Brunner, Julian;Lammich, Peter
• 通讯作者: Lammich, Peter