Home > Authorities > Grants > Record #521227
 

DFG project G:(GEPRIS)183790222

Computergestützte Verifikation von Automatenkonstruktionen für Model Checking

CoordinatorProfessor Dr. Javier Esparza ; Professor Dr. Bernhard Nebel ; Professor Dr. Tobias Nipkow, Ph.D.
Grant period2010 - 2019
Funding bodyDeutsche Forschungsgemeinschaft
 DFG
IdentifierG:(GEPRIS)183790222

Note: 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.
   

Recent Publications

There are no publications

 Record created 2023-02-02, last modified 2024-09-27
Similar records



Rate this document:

Rate this document:
1
2
3
4
5
 
(Not yet reviewed)
PUBDB :: Search :: Submit :: Personalize :: Help
Powered by Invenio v1.1.7 | join2_v2508a
Maintained by l.pubdb@desy.de

Impressum | Data Privacy Policy