Skip to main content Skip to main navigation

Project | Verisoft XT

Duration:
Verisoft XT

Verisoft XT

Verisoft XT is a three-year research project funded by the German Federal Ministry of Education and Research (BMBF). Project management agency is the German Aerospace Center (DLR). The main goal of the project is the pervasive formal verification of computer systems. The correct functionality of systems, as they are used, for example, in automotive engineering, in security technology and in the sector of medical technology, is to be mathematically proved.

The proofs are computer aided in order to prevent human error by the scientists involved. The knowledge and progress obtained are expected to assist german enterprise in achieving a stable, internationally competitive position in the professional areas mentioned above.

The Verisoft XT project is focused on:

  • The creation of methods and tools which would allow the pervasive formal verification of the design of integrated computer systems.
  • An increase in industrial productivity and quality.
  • The prototypical realization of four concrete, industrial application tasks.

Verisoft XT is the successor project of Verisoft. It is planned over three years and approved by the BMBF (period of validity: 01.07.2007 - 30.06.2010).

Partners

  • 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

Publications about the project

  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.

Sponsors

BMBF - Federal Ministry of Education and Research

BMBF - Federal Ministry of Education and Research