Skip to main content Skip to main navigation

Projekt | Verisoft XT

Laufzeit:
Verisoft XT

Verisoft XT

Verisoft XT ist ein über drei Jahre angelegtes Forschungsprojekt, das vom Bundesministerium für Bildung und Forschung (BMBF) gefördert wird. Projektträger ist das Deutsche Zentrum für Luft- und Raumfahrttechnik (DLR). Ehrgeiziges Projektziel ist die durchgängige, formale Verifikation von Computersystemen: die korrekte Funktionsweise von Systemen, wie sie beispielsweise im Automobilbau, in der Sicherheitstechnologie und auf dem medizinisch-technischen Sektor zum Einsatz kommen, soll mathematisch bewiesen werden.

Die Beweise werden dabei computergestützt geführt, um menschliches Versagen der beteiligten Wissenschaftler nach Möglichkeit auszuschließen. Die gewonnenen Erkenntnisse und erzielten Fortschritte sollen dabei helfen, deutschen Unternehmen aus diesen Sparten dauerhafte internationale Wettbewerbsvorteile zu schaffen.

Die Leitvorstellung des Vorhabens Verisoft XT besteht darin:

  • die Methoden und Werkzeuge zu schaffen, die es gestatten, das Design von integrierten Computersystemen durchgehend formal zu verifizieren,
  • dadurch einen Produktivitäts- und Qualitätshub für die Industrie zu generieren, und
  • dieses an vier konkreten, industriellen Anwendungsszenarien prototypisch zu realisieren.

Verisoft XT ist das Nachfolgeprojekt von Verisoft. Es ist über drei Jahre angelegt und durch das BMBF bewilligt (Laufzeit: 01.07.2007 - 30.06.2010).

Partner

  • AbsInt Angewandte Informatik GmbH
  • AUDI AG
  • Robert Bosch GmbH
  • Concept of Truth
  • DFKI
  • EMIC European Microsoft Innovation Center
  • Elektroniksystem- und Logistik-GmbH
  • Infineon Technologies AG
  • OneSpin Solutions GmbH
  • SIRRIX AG security technologies
  • SYSGO AG
  • TÜV SÜD Automotive GmbH
  • Technische Universität München
  • Universität Bremen
  • Universität Koblenz-Landau
  • Universität des Saarlandes
  • Albert-Ludwigs-Universität Freiburg

Publikationen zum Projekt

  1. VCC: A Practical System for Verifying Concurrent C

    Ernie Cohen; Markus Dahlweid; Mark Hillebrand; Dirk Leinenbach; Michael Moskal; Thomas Santen; Wolfram Schulte; Stephan Tobies

    In: Stefan Berghofer; Tobias Nipkow; Christian Urban; Makarius Wenzel (Hrsg.). Theorem Proving in Higher Order Logics, 22nd International Conference. International Conference on Theorem Proving in Higher Order Logics (TPHOLs-09), August 17-20, Munich, Germany, Pages 23-42, Lecture Notes in Computer Science (LNCS), Vol. 5674, ISBN 978-3-642-03358-2, Springer, 8/2009.
  2. Formal Verification of a Reader-Writer Lock Implementation in C

    Mark Hillebrand; Dirk Leinenbach

    In: Proceedings of the 4th International Workshop on Systems Software Verification. International Workshop on Systems Software Verification (SSV-2009), June 22-24, Aachen, Germany, Pages 123-141, Electronic Notes in Theoretical Computer Science, Vol. 254, Elsevier Science B.V. 2009.
  3. Verifying the Microsoft Hyper-V Hypervisor with VCC

    Dirk Leinenbach; Thomas Santen

    In: 16th International Symposium on Formal Methods. International Symposium on Formal Methods (FM-2009), November 2-6, Eindhoven, Netherlands, Pages 806-809, Lecture Notes in Computer Science, Vol. 5850, Springer, 2009.

Fördergeber

BMBF - Bundesministerium für Bildung und Forschung

BMBF - Bundesministerium für Bildung und Forschung