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:
- Formal methods for the analysis and verification of software systems.
- 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
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.
© Copyright University of Essex. All rights reserved.
This page was last modified by
Norbert Völker on 10 Nov 2008
University of Essex, School of Computer Science
and Electronic Engineering