Norbert Völker - Research Page

Dr.-Ing. Norbert Völker

Foundations and Applications Research Group

Contact details

Current Teaching

Research Interests

Theorem proving, especially in higher order logic (HOL) and using the Isabelle theorem proving assistant.
- HOL2P - an extension of classical higher order logic with universal types and type operator variables
E-business and E-commerce applications:
- InterPROM: Interoperable Collaborative Process Management
- Development of e-business/ e-commerce/ e-government toolkits with ARFS (TCS Project 3830, KTP Project 534).
Formal methods for the analysis and verification of software systems.
- Constructive Z, RefineNet
Development of embedded software systems

Publications ( bibtex)

N.Völker. HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism, Proceedings of TPHOLs'07, Kaiserslautern, Germany, LNCS 4732, 2007.
L. Cragg, H. Hu, N.Völker. Modularity and Mobility of Distributed Control Software for Networked Robots. In: Software Engineering for Experimental Robotics, Springer Tracts on Advanced Robotics Volume 30, Davide Brugali (Ed), 459-484, 2007.
Carsten Huth, Norbert Völker, Olaf Hahnl, Björn Reinhold. INTERPROM - A Collaborative Framework Driven by Business Needs, ICE-B, 2006 (presentation).
H. Hu, P.W. Tsui, L. Cragg, N. Völker. Agent architecture for multi-robot cooperation over the Internet. Integrated Computer-Aided Engineering, Volume 11(3), 213 - 225, 2004.
N. Völker. Thoughts on Requirements and Design of User Interfaces for Proof Assistants, UITP 2003, ENTCS, Volume 103, 139-159, 2004.
N. Völker and B.J. Krämer. Automated verification of function block-based industrial control systems. Science of Computer Programming, 42, 101-113, 2002.
N. Völker. Two Semantic Embeddings of Z Schemas in Isabelle/HOL, Technical Report CSM-344, Department of Computer Science, University of Essex, 2001.
N. Völker. A Deep Embedding of ZC in Isabelle/HOL, Technical Report CSM-343, Department of Computer Science, University of Essex, 2001.
N. Völker. Towards a HOL Framework for the Deductive Analysis of Hybrid Control Systems. ADPM2000: 4th International Conference on Automation of Mixed Processes, Dortmund, Germany, 18-19 September 2000.
N. Völker and H.-F. Kötter. FCell3D: A Central Example to Visualize Safety Critical Processes in the Construction and Control of Distributed Applications, M/SET 2000, San Diego, February 2000.
N. Völker. Disjoint Sums over Type Classes in HOL. Proceedings of TPHOLs'99, Nice, France, LNCS 1690, 5 - 18, 1999.
H.-F. Kötter, B. Krämer, N. Völker. 3D-Visualisierung sicherheitskritischer Vorgänge in der Lehre mittels Java und VRML. Presented at: Simulation und Visualisierung'99, Magdeburg, March 1999.
Norbert Völker. Ein Rahmen zur Verifikation von SPS-Funktionsbausteinen in HOL. PhD thesis, 1998.
B.J. Krämer, N. Völker, R. Lichtenecker, and H.-F. Kötter. Deriving CORBA Applications from Formal Specifications. Journal of Systems Integration, 8, 1-16, 1998.
B.J. Krämer and N. Völker. A Highly Dependable Computer Architecture for Safety-Critical Control Applications. Real-Time Systems Journal, 13(3), 237-251, 1997.
W.A. Halang, B.J. Krämer and N.Völker. Formale Verifikation der Grundelemente in Funktionsplänen von Notabschaltsystemen. In: Verläßliche IT-Systeme, 229-250, H.H. Brüggemann und W.Gerhardt-Häckl (Eds.), Braunschweig-Wiesbaden: Viehweg Verlag, 1995.

Miscellaneous

Essex Dependable System Group Postgraduate Seminar in May 2004, part of the TCS-SOUP programme (Theoretical Computer Science for SOuth-eastern Universities PhD students).

Copyright Notice

The documents contained on this webpage are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit written permission of the copyright holder.