Georg Rock |
|
Dr. Georg Rock |
|
Research areas
· Deduction:
- Automatic Theorem
Proving
- Tactical Theorem
Proving
- Interactive Theorem
Proving
· Security, Formal methods
- Cryptographic Protocols
- Security Policies,
Information Flow Control
- Real-Time Requirements
Engineering
- Formal Methods in
Software Engineering
Some actual projects
- VERISOFT (BMBF)
Verification of large industrial software
- MRTD-I, MRTD-II (BSI)
Verification of Security Protocols for MRTD’s
- CBI (T-Systems, BMBF)
Verification of Chipcard based
Biometric Identification System as part of the VERISOFT project - TokenProtect (BSI) Verification
of Security Protocols in Sensor Networks
- Valikrypt (BSI)
Validation and Verification of Security Protocols
Tools
- Verification Support
Environment (VSE)
Selected
publications
- Lassaad Cheikhrouhou, Georg Rock, Werner Stephan, Matthias Schwan, Gunter Lassmann:
Verifying a Chip-Card-Based Biometric Identification Protocol in VSE, The
25th International Conference on Computer Safety, Security and Reliability
(SAFECOMP 2006), 26-29 September 2006,
- Gunter Lassmann, Georg Rock, Matthias Schwan,
Lassaad Cheikhrouhou: Verisoft Secure Biometric Identification
System, T-Systems International University Conference,
Düsseldorf, 10.-11.10.2005, to be published, draft version: Verisoft_CBI_System_v101.pdf.
- Andreas Nonnengart, Georg Rock, Werner Stephan: Verification
Support Environment (VSE), Fourth International Workshop
on Planning and Scheduling for Space - IWPSS '04, WPP-228
- Serge Autexier, Dieter Hutter,
Bruno Langenstein, Heiko Mantel, Georg Rock, Axel Schairer,
Werner Stephan, Roland Vogt, and Andreas Wolpers.
VSE: Formal methods meet
industrial needs. International Journal on Software Tools for Technology
Transfer, Special Issue on Mechanized Theorem Proving for Technology,
3(1), 2000.
- Dieter Hutter, Bruno Langenstein, Georg Rock, Jörg Siekmann, Werner Stephan, and Roland Vogt. Formal software development in
the verification support environment. Journal of Experimental and
Theoretical Artificial Intelligence, 2000. accepted, forthcoming.
- Dieter
Hutter, Heiko Mantel, Klaus-Peter Jantke, Georg Rock, and Werner Stephan. Automated reasoning for system
verification: A tutorial introduction into VSE-II. In Proceedings Ilmenau International Scientific Colloquium, Special
Track: Validation and Verification, 2000.
- Dieter
Hutter, Georg Rock, Jörg Siekmann, Werner Stephan, and Roland Vogt. Formal software development in
the Verification Support Environment (VSE). In Proceedings 13th
International
- Georg
Rock, Werner Stephan, and Michael Brodski. Modeling, specification and
verification of an emergency closing system. In FLAIRS-2000, Special
Track on Verification, Validation and System Certification, 2000. The
13th International FLAIRS Conference, Orlando, Florida.
- Dieter Hutter, Heiko Mantel, Georg Rock, Werner Stephan,
Andreas Wolpers, Michael Balser, Wolfgang Reif,
Gerhard Schellhorn, and Kurt Stenzel. VSE: Controlling the complexity in formal
software developments. In D. Hutter, W. Stephan,
P. Traverso, and M. Ullmann, editors, Proceedings Current Trends in
Applied Formal Methods, FM-Trends 98,
- Georg
Rock, Werner Stephan, and Andreas Wolpers. Modeling
Dynamic Processes in TLA. In Katharina Spies and Bernhard Schätz (Hrsg.),
editors, FBT'99. Formale Beschreibungstechniken für
verteilte Systeme, pages 185-192. Herbert Utz Verlag, 1999. 9. GI/ITG-Fachgespräch,
München.
- Georg
Rock, Werner
Stephan, and Andreas Wolpers. Modular Reasoning about
Structured TLA Specifications. In R. Berghammer
and Y. Lakhnech, editors, Tool Support
for System Specification, Development and Verification, Advances in
Computing Science, pages 217-229. Springer, 1999.
- Georg
Rock, Werner Stephan, Andreas Wolpers, Michael Balser, Wolfgang Reif, and
Stefan Scheer. Structured formal development in vse-II: The robertino case
study. In
Sicherheit und Zuverlässigkeit software-basierter Systeme,
Bericht ISTec-A-367, pages 138 -- 152.
Gemeinsamer Workshop der GI-Fachgruppen: Alternative Konzepte für
Sprachen und Rechner (2.1.4) und German ENCRESS (3.6.2), Francesca Saglietti and Wolfgang Goerigk,
1999.
- Andreas Nonnengart, Georg Rock, and Christoph Weidenbach. On generating small
clause normal forms. In Proceedings of the 15th International Conference on
Automated Deduction, CADE98, volume 1421 of LNCS, pages
397-411. Springer, 1998.
- Georg
Rock, Werner Stephan, and Andreas Wolpers. Assumption-commitment
specifications and safety-critical systems. In Hartmut
König and Peter Langendörfer,
editors, FBT'98. Formale Beschreibungstechniken für
verteilte Systeme, pages 125-135. Shaker
Verlag, Aachen, 1998. 8. GI/ITG-Fachgespräch.
- Georg Rock, Werner Stephan, and Andreas Wolpers.
Tool support
for the compositional development of distributed systems. In A. Wolisz, I. Schieferdecker,
and A. Rennoch, editors, 7. GI/ITG
Fachgespräch: Formale Beschreibungstechniken für verteilte
Systeme. GMD-Studien Nr. 315, 1997.
- Weidenbach
C., Gaede B., and Rock G. SPASS & FLOTTER, version 0.42. In M. McRobbie and J. Slaney,
editors, 13th International Conference on Automated Deduction, CADE-13,
volume 1104 of LNAI, pages 141-145. Springer, 1996.
- Georg. Rock. Transformations of
first-order formulae for automated reasoning. Masters Thesis.
Max-Planck-Institut für
|
Letzte Änderung:
18.03.2007 |
