Holger Pfeifer
|
Dr. Holger Pfeifer
Institute of Artificial Intelligence
Universität Ulm
D-89069 Ulm
|
|
O 27 / 446
|
|
(+49) 731 / 50 - 24124
|
|
(+49) 731 / 50 - 24119
|
|
Holger.Pfeifer@uni-ulm.de
|
|
|
My research centres around applying formal methods and
theorem proving to
model and analyse various types of systems, with a special
emphasis on the fault-tolerant and safety-critical domain.
Current projects:
Projects that I have been working on:
I was also partially involved in the following projects:
- H. Pfeifer, F. von Henke
Modular Formal
Analysis of the Central Guardian in the Time-Triggered
Architecture
Reliability Engineering & System Safety, 92(11):1538-1550, Nov. 2007
Special Issue on Safety, Reliability and Security of Industrial
Computer Systems, Elsevier Ltd.
This is an extended version of a paper presented at SAFECOMP
2004.
- H. Pfeifer, F. von Henke
Formal Modelling and
Analysis of Fault Tolerance
Properties in the Time-Triggered Architecture
5th Symposium on Formal Methods for Automation and Safety
in Railway and Automotive Systems
(FORMS/FORMAT)
Braunschweig, Germany, December 2-3, 2004
- H. Pfeifer, F. von Henke
Modular Formal
Analysis of the Central Guardian in the Time-Triggered
Architecture
23rd International Conference on
Computer Safety, Reliability and Security
(SAFECOMP)
Potsdam, Germany, September 21-24, 2004
- T. Liebig, H. Pfeifer, F. von Henke
Reasoning Services for an OWL
Authoring Tool: An Experience Report
Proc. of DL2004, June 2004
- W. Steiner, J. Rushby, M. Sorea, H. Pfeifer
Model Checking a Fault-Tolerant
Startup Algorithm:
From Design Exploration To Exhaustive Fault Simulation
Proc. of
DSN 2004, pp. 189-198,
June/July 2004
- H. Pfeifer
Formal Analysis of
Fault-Tolerant Algorithms in the Time-Triggered Architecture
PhD Thesis, Univ. Ulm, 2003
- H. Pfeifer, F. von Henke
Formal Analysis for Dependability
Properties: the Time-Triggered Architecture Example
Proc. of
ETFA 2001.
IEEE Computer Society, pp. 343-352, October 2001
-
H. Pfeifer
Formal Verification of the TTP Group
Membership Algorithm
Proc. of
FORTE/PSTV 2000.
Kluwer Academic Publishers, pp. 3-18, October 2000.
-
H. Pfeifer, H. Rueß
Polytypic Proof Construction
Proc. of TPHOLs'99.
Springer LNCS 1690, pp. 55-72, September 1999
-
H. Pfeifer, D. Schwier, F. W. von Henke
Formal Verification for
Time-Triggered Clock Synchronization
Proc. of Dependable Computing for Critical Applications 7
(DCCA 7)
IEEE Computer Society, Dependable Computing and Fault-Tolerant Systems
Series, pp. 207-226, January 1999.
-
F. W. von Henke, S. Pfab, H. Pfeifer, H. Rueß
Case Studies in Meta-Level Theorem Proving
Proc. of TPHOLs'98,
Springer LNCS 1479, pp. 461 - 478, September 1998
-
H. Pfeifer, H. Rueß
Polytypic
Abstraction in Type Theory
Informal Proc. of Workshop on Generic Programming (WGP'98). Marstrand, Sweden, 18 June 1998.
-
A. Dold, F. W. von Henke, H. Pfeifer, H. Rueß
Formal Verification of Transformations
for Peephole Optimization
Proc. of FME'97, Springer LNCS 1313, pp. 459 - 472, September 1997
-
F.W. von Henke, M. Luther, H. Pfeifer, H. Rueß, D. Schwier,
M. Strecker, M. Wagner
The Typelab Specification and
Verification Environment
Proc. of AMAST'96, Springer LNCS 1101, pp. 604-607, Munich, 1996
-
F. Bartels, H. Pfeifer, F. W. v. Henke, and H. Rueß
Mechanizing Domain
Theory
Technical Report UIB-96-10, Universität Ulm, 1996
Revised version as of
October 1997.
-
H. Pfeifer, F. W. v. Henke, and H. Rueß
Guided Tour Through a Mechanized Semantics of Simple Imperative Programming Constructs
Technical report UIB 96-11, Universität Ulm, Fakultät für
Informatik, Dec. 1996
Revised version as of July 1997
- A. Dold, F. W. von Henke, H. Pfeifer, H. Rueß
Generic Compilation Schemes for Simple Programming Constructs
Technical report UIB 96-12, Universität Ulm, Fakultät für Informatik,
Dec. 1996
Revised version as of Jan. 1999
-
H. Rueß, H. Pfeifer, F.W. von Henke
Formalization and
Reasoning in a Reflective Architecture
Proc. of the IJCAI 1995 Workshop on
Reflection and Meta Level Architecture and their Application in AI
Montreal, Canada, August 1995
Betreuung von Lehrveranstaltungen:
