Zum Hauptinhalt springen

Universität Ulm

Universität Ulm
Fakultät für Informatik 
Abt. Programmiermethodik und Compilerbau 

Prof. Dr. Wolfgang Reif

 

Arbeitsschwerpunkte

Grundlagen der Softwaretechnik, Sichere Software, Formale Methoden (Modellierung, Verifikation, Deduktion), KI-Methoden im Software-Engineering, Werkzeugentwicklung und Anwendungen.

Projekte

  • KIV - Eine Umgebung zur Entwicklung korrekter Systeme. Von den informellen Anforderungen bis zum verifizierten Code. Langjährig gefördert von der Deutschen Forschungsgemeinschaft (DFG), dem Bundesministerium für Bildung, Wissenschaft, Forschung und Technologie (BMBF) und dem Land Baden-Württemberg.
  • VSE-II - Verifikation nebenläufiger, reaktiver Systeme. Gefördert vom Bundesamt für Sicherheit in der Informationstechnik (BSI). Weitere Projektpartner sind das Deutsche Forschungszentrum für Künstliche Intelligenz (DFKI GmbH, AG Prof. Dr. Siekmann) sowie die Firma Innovative Software Technologie (IST GmbH).
  • Integration automatischer und interaktiver Beweisführung. Gefördert von der DFG im Schwerpunktprogramm Deduktion. Projektpartner ist die Universität Karlsruhe (Prof. Dr. Menzel, Prof. Dr. Schmitt, PD Dr. Hähnle)

Veröffentlichungen

  • Wolfgang Reif, Software-Verifikation und ihre Anwendungen, it+ti Themenheft 3/97: Formale Entwurfsmethoden - Software Correctness, Oldenbourg Verlag, 1997.
  • Wolfgang Reif, The KIV-approach to Software Verification, in KORSO: Methods, Languages, and Tools for the Construction of Correct Software - Final Report, M. Broy and S. Jähnichen (eds.), Springer LNCS 1009, 1995.
  • W. Reif, G. Schellhorn, K. Stenzel, M. Balser, Structured Specifications and Interactive Proofs with KIV, Automated Deduction - A Basis for Applications, W. Bibel, P. Schmitt (eds.), Kluwer Academic Publishers, 1998.
  • W. Reif and G. Schellhorn and K. Stenzel, Interactive Correctness Proofs for Software Modules Using KIV, Tenth Annual Conference on Computer Assurance, NIST, Gaithersburg (MD), USA IEEE press, 1995.
  • W. Reif and K. Stenzel, Reuse of Proofs in Software Verification, Foundation of Software Technology and Theoretical Computer Science, Bombay, India, R. Shyamasundar (ed.), Springer LNCS 761, 1993.
  • G. Schellhorn and W. Ahrendt, Reasoning about Abstract State Machines: The WAM Case Study, Journal of Universal Computer Science (J.UCS), 1997.

     

Produkte und Werkzeuge

KIV

KIV ist ein fortgeschrittenes Werkzeug zur Entwicklung sicherheitskritischer Software. Das Werkzeug unterstützt die formale Modellierung von Software- und Systemdesigns, die Spezifikation von Sicherheitsmodellen, formale Validierung von Spezifikationen und den Nachweis von Sicherheitsmodellen. Spezifikationskomponenten werden durch Softwaremodule schrittweise implementiert und formal verifiziert. Es wird der gesamte Entwicklungsprozess von den informellen Anforderungen bis zum verifizierten Code unterstützt. Neben dem Einsatz in realen Anwendungsprojekten in der Industrie ist KIV auch für die Lehre interessant (z.B. Kurse und Praktika zum Thema Spezifikation und Verifikation).

VSE

VSE ist ein Verifikationswerkzeug, das es ermöglicht, formale und konventionelle Softwareentwicklung zu verzahnen. Als Verifikationskomponenten werden Grundversionen von KIV und INKA (DFKI) verwendet. VSE wird von der Universität Ulm, dem DFKI und der Firma IST in Lizenz des BSI kommerziell vertrieben.

 

Kontaktadresse:

Prof. Dr. Wolfgang Reif
Universität Ulm
Fakultät für Informatik 
Abt. Programmiermethodik und Compilerbau
James-Franck-Ring, 89069 Ulm
Tel.: (0731) 502-4161
Fax: (0731) 502-4162
reif@informatik.uni-ulm.de