Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Via: uk.ac.rhbnc.dcs; Mon, 29 Mar 1993 18:13:40 +0100
From: Vicky Stavridou <victoria@uk.ac.rhbnc.dcs>
Date: Mon, 29 Mar 93 18:06:44 BST
Message-Id: <20685.9303291706@white.cs.rhbnc.ac.uk>
To: Edmund.Clarke@EDU.CMU.CS.GP.G, JON@edu.washington.radonc.gaffer, 
    R_Witty@it.jrc.cen, S.M.S.Syed-Mustaffa@uk.ac.soton.ecs, 
    Tobias.Nipkow@de.tu-muenchen.informatik, Tom.Anderson@uk.ac.ncl, 
    ac@uk.co.hp.hpl, anti@ua.kiev.icyb.d245, apr@dk.dth.id, baw@uk.co.npl.seg, 
    borrione@fr.imag.imag, bowen@uk.ac.ox.prg, carh@uk.ac.ox.prg, cha@org.aero, 
    claesen@be.imec, cliff@uk.ac.man.cs.ux, courcou@gr.forth.csi.terpsi, 
    csjvt@uk.ac.swan.pyr, dad@uk.ac.rl.inf, dan@ca.on.ora, dc@uk.co.hp.hpl, 
    inmos!des@uk.ac.cam.cl, dhp@uk.ac.cs.surrey, dhp@uk.ac.surrey.cs, 
    doug@uk.ac.man.cs, eker@fr.loria, eswjc@uk.ac.warwick, fkh@uk.ac.ukc, 
    futatsugi@jp.go.etl, gcs@uk.ac.bath.maths, germaine@nl.kun.cs, 
    glc@uk.ac.ed.dcs, goguen@uk.ac.ox.prg, grud@ua.kiev.icyb.d245, 
    guttag@edu.mit.lcs.larch, howard@uk.ac.man.cs, hunt@com.cli, 
    info-hol@edu.uidaho.cs.ted, joyce@ca.ubc.cs, jst@dk.dth.id, 
    kapur@edu.albany.albanycs, lescanne <lescanne%poincare.crin.fr@uk.ac.ukc>, 
    leveson@edu.washington.cs, liskov@edu.mit.lcs.proton, mcg@fr.lri.lri, 
    mikef@uk.ac.ed.lfcs, milne@uk.ac.strath.cs, Mike.Gordon@uk.ac.cam.cl, 
    moriconi@com.sri.csl, musser@edu.rpi.cs, n.e.fenton@uk.ac.city, 
    prinetto%itopoli.BITNET@edu.cuny.cunyvm, pygott@uk.mod.hermes, 
    rushby@com.sri.csl, ryan@uk.mod.hermes, sb@com.hp.hpl.hplb, 
    sd396@uk.ac.city, sifakis@fr.imag.vercors, soulas@fr.edf.der.rem63ax, 
    sufrin@uk.ac.ox.prg, Tom.Melham@uk.ac.cam.cl, ttercs@uk.co.lreg.aie, 
    vassiliou@gr.forth.csi.terpsi, williamsg@ca.aecl.crl.cc49, 
    xbr4d75r%ddathd21.BITNET@edu.cuny.cunyvm, zedan@uk.ac.york.minster
Subject: Lectureship at Royal Holloway

We are currently recruiting for a lectureship in Computer Science. The main
expertise domain is formal methods. I would be grateful if you could bring
the attached to the attention of anyone who you think might be interested
in the position.

Thank you for your help,

Victoria Stavridou
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Dr Victoria Stavridou,                  || Email victoria@uk.ac.rhbnc.cs
Department of Computer Science,         || ===== 
Royal Holloway and Bedford New College, || Phone (+44) 784 443429/21   
University of London,                   || =====
Egham,                                  || Fax   (+44) 784 443420 
Egham Hill,                             || ===
Surrey TW20 0EX,                        || Home  (+44) 793 496272
UNITED KINGDOM.                         || ====
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
\documentstyle[11pt]{article}
\input a4l

\parskip=1ex
\parindent=0pt
\title{
{\bf Royal Holloway, University of London}\\~\\
Appointment details\\
{\bf LECTURER IN COMPUTER SCIENCE}}
\author{}

\begin{document}

\maketitle

Applications are invited for the above post from candidates with an outstanding research record in Computer Science.

Existing research specialities of the department include: Probabilistic Inference, Applied Formal Methods, Information Security, Connection Science and Computational Learning Theory.  The expanding Department of Computer Science is part of the Science Faculty of one of the five designated science sites of London University.  The location at Egham provides an attractive environment and opportunities for close industrial collaboration.

Applications are particularly welcome from candidates with research interests relating to one of the two following fields, in which the department wishes to expand its existing research activity.
\begin{itemize}
\item Formal methods of system specification and verification with particular emphasis on safety critical systems applications.
\item Computational models of probabilistic reasoning and learning in Bayesian belief networks.
\end{itemize}

The appointment will be made on the Lecturer A scale \pounds15,534--\pounds20,710 a year, inclusive of London Allowance.

Informal enquiries may be made to Professor Chris Mitchell (tel.\ 0784 443423).

Further particulars and application forms are available from the Personnel Office, Royal Holloway, University of London, Egham, Surrey TW20 0EX.  Telephone 0784 443030.  Fax: 0784 472005.

The closing date for receipt of applications is 19th April 1993.

\section*{Royal Holloway}

\begin{enumerate}

\item[1.] Royal Holloway is a School of the University of London with Faculties of Arts and Science.  It occupies a delightful campus at Egham, Surrey, situated in the Green Belt near Runnymede and Windsor Great Park, with good communications to and from London.  Egham is 35 minutes by train from Waterloo and the College is one mile from the M25 and 15 minutes' drive from Heathrow airport.

\item[2.]  The College has a student population of 4,200 and recruitment is buoyant.  There are 18 academic departments in the Faculties of Science and Arts \& Music, and a total of 260 academic teaching staff.

\end{enumerate}

\section*{The appointment}

\begin{enumerate}

\item[3.] The starting salary for the appointment will be on Lecturer Grade A within the range \pounds15,534--\pounds20,710 a year, inclusive of London Allowance.

\item[4.] The closing date for applications is April 19th 1993.

\item[5.] The provisional date for interviews is May 27th 1993.

\item[6.] The lectureship is available from 1st October 1993.

\item[7.] Application forms (two copies) should be returned to the Personnel Officer, Royal Holloway, University of London, Egham, Surrey TW20 0EX.

\end{enumerate}

\section*{Extract from equal opportunities policy}

\begin{enumerate}

\item[8.] The only consideration in recruitment of employees will be how the genuine requirements of the post are met or likely to be met by the individual under consideration.  These requirements, including retirement at the appropriate age, being met, no regard will be taken (except where legally required) of that person's race, sex, age, marital status, number of children, physical disability or beliefs or lawful preferences, privately held on any matter including religion, politics and sex.

\end{enumerate}

\section*{Smoking policy}

\begin{enumerate}

\item[9.] In an effort to provide a healthy and comfortable working environment, smoking is prohibited in public areas.  Open plan and shared areas are non-smoking unless everyone is in agreement.  Private offices may be designated as smoking by the occupant.  Full details of the Smoking Policy are available from the College Safety Officer.

\end{enumerate}

\section*{Other information}

\begin{enumerate}

\item[10.] The Department of Computer Science is located in a new building
near the Centre of the Campus and close to the College Computer
Centre.  The department has thirteen established academic posts in
Computer Science, including the currently advertised lectureship.

The
Department's undergraduate teaching load at present is around 170 Full Time
Equivalent (FTE) students.  The Department's post-graduate teaching load is currently approaching 20 students, roughly equally divided between taught and research.
  
\item[11.] The department is well equipped with computer work-stations for
teaching and research.  Following a major re-equipment of the under-graduate teaching laboratories, which took place in the summer of 1991, the department has between 60 and 70 seats equipped with 19-inch screens running
Unix.  The standardised user interface is Motif
running on X-windows.  All staff who do not have equipment provided under personal research grants are provided with a 19-inch Unix work-station or X-terminal.

In addition to the departmental provision, individual research groups possess a network of SUN workstations, nine HP-UX workstations and a number of DECstations.

There is a campus network
interconnected to the University of London
Computer Centre and all other centres.  The College
Computer Centre, which is separate from the department,
has a VAX 6430 and several workstations.

\end{enumerate}

\pagebreak

\begin{center}
{\Huge The Computer Science Department}
\end{center}

\section{Members of staff and their work}

\subsection*{Dave Cohen, BA, DPhil Oxon.}

The application of Mathematics within Computer Science and the theory of neural
networks.


\subsection*{Alan Davies, BSc, MSc Lond.}

Computer modelling of large scale scientific problems especially in the field 
of laser optics and wave guides.

\subsection*{Roy Edwards, DFH, AMIEE, MBCS}

Functional programming and its implementation.


\subsection*{Professor Alex Gammerman, BSc, PhD Leningrad, FRSS, MBCS}

Probabilistic inference and learning.  Use of Bayesian belief networks.

\subsection*{Dieter Gollmann, Dipl.-Ing., Dr.techn Linz, Dr.habil Karlsruhe}

Cryptography, information security, algorithm engineering, and VLSI design.


\subsection*{Liz Hogger, BSc, MSc Lond., BA Open, ARCS, DIC}

Algorithmic machine learning, and its relationship to non-monotonic logic: 
with particular application to learning heuristics for meta-level control of
logic programs, and for other problems involving selection from multiple 
entities.


\subsection*{Pete Jeavons, MA Oxon, MSc Leic., PhD Lond., GIMA}

Constraint networks, neural networks, 
and the mathematical foundations of connectionism.


\subsection*{Adrian Johnstone, BSc, PhD Lond.}

Multiprocessor systems for
real-time machine vision.  Language design for multiprocessor and
array processor systems.  VLSI implementation of image processing
algorithms and advanced processors.


\subsection*{Professor Chris Mitchell, BSc, PhD Lond., CEng, CMath, FBCS, FIEE, FIMA}

Information security, including communication security, secure protocols and
cryptography; information theory.


\subsection*{Sean Murphy, BA Oxon, PhD Bath}

Cryptology, especially encryption algorithms, and 
spatial probability and statistics.  (Dr.\ Murphy is a joint appointment with Mathematics).


\subsection*{John Shawe-Taylor, PhD, MSc Lond., DIC, CMath}

Parallel distributed processing; 
the mathematical analysis of learning in neural nets;  
learning algorithms; computational learning theory; neural network chip design.


\subsection*{Vicky Stavridou, BSc, MSc Salford,
PhD Manchester, CEng, MIEE}

Specification, development and assessment of safety
critical systems;
specification and verification of digital systems;
requirements engineering;
automated theorem proving.

\subsection*{Max van Daalen, BSc Lond., AMIEE}

Neural networks (hardware implementation), array processors architecture 
(VLSI), machine vision algorithms and their hardware implementation.

\section{Research group profiles}

\subsection{Probabilistic Inference}

Research in probabilistic inference and learning concentrates around development
of exact and approximate algorithms for
Bayesian belief networks to handle mixed models
and their implementations in the
computational systems.
In the case of the exact approach the model of Conditional
Gaussian  distribution and linear
relationships is used. The application of stochastic simulation to mixed graphical
association models enables to estimate marginal densities of continuous variables.

There is a number of applications of this research in different fields such as medicine,
forensic science, and biological taxonomy. One of the projects, called LIKELY, aims to combine
model-based predictions with the experience of forecasters in order to improve the accuracy of forecasting procedures. The project is funded under the auspices of the EEC
DOSES programme.  Another project is being developed with a local hospital. The aim is 
to develop a probabilistic system without assuming independence between symptoms for diagnosis of set of diseases.

\subsection{Formal Methods}

The Formal Methods Group has an international reputation in the field of
formal methods in Computer Science and is substantially supported by
ESPRIT and IED/SERC funds. The group has a strong background in safety
critical systems, the theory and practice of 
equational reasoning, theorem proving, hardware verification
and algebraic specification languages, particularly OBJ3 and FUNNEL.
The mission of the group is to investigate ways of using formal techniques in
order to improve the development process of systems. The group is
concentrating to three application domains, namely synchronous digital
systems, real--time systems and high integrity systems. The group is led by
Dr Victoria Stavridou and currently consists of four funded research
assistants, a doctoral student and a secretary. Group members are
supported by an extensive network of Sun workstations.

We place particular emphasis on
industrial collaboration in order to assist our application--oriented
objectives. We have strong collaborative links with the Information
Security Group at Royal Holloway, the Programming Research
Group at Oxford 
University, the Centre for Software Reliability of City University,
the Centre for Human Computer Interface Design of City University,
the Department of Mathematics and Computer Science of 
University College Swansea, the Department of Computer Science of the
Technical University of Denmark, the Computer Science Laboratory of
SRI International in California, DRA Malvern, NPL, Inmos, Lloyd's Register,
GEC Avionics and the Safety 
and Reliability Directorate of the UK Atomic Energy Authority.

The group is currently involved in the following projects:

\subsubsection{SSVE}
The hardware specification and verification activities at RHUL are
based on algebraic methods and are primarily centered around the
provision of translators and theorem proving tools. The IED/SERC
SSVE project (An integrated hardware specification, simulation and
verification environment) aims to 
develop an integrated environment suitable for industrial use, that
supports all three activities associated with the design of digital
systems: specification, simulation and formal verification. The
project intends to bridge the gap between successful large scale
verification attempts (such as the VIPER project) and the almost
non--existent impact of formal methods on everyday designer practice.
We have produced FUNNEL, a new hardware description language with
formal semantics and 2OBJ, a generic theorem proving tool based on the
algebraic specification language OBJ3.
The lead partner is the Applied Formal Methods Group  at RHUL. The
consortium consists of RHUL, the Programming Research Group at the
University of Oxford, {\large {\sf inmos}} and the Computing
 Division of DRA, Malvern.

\subsubsection{NewThink}
NewThink (Orwellian Specifications for Safety Critical Systems) is
sponsored by SERC and the National Physical Laboratory. The work 
 concentrates on three aspects: The 
development of a formal requirements capture language and its
transformation to a formal program specification satisfying the
requirements, orwellian specifications for safety critical systems and
the development of Defence standards on the procurement of safety
critical software. The project has produced a  formalisation of
requirements satisfying the UN explosive regulations which
will be used by the MOD Directorate of Proof and Experimental
Establishments for future tenders in the spirit of the recent interim
MOD standard 00--55 on the procurement of safety critical software. We
are currently working on 
NewThink, an orwellian real--time subset of VDM which will be used to
express specifications which will then be transformed to NewSpeak
programs. In order to facilitate such transformations, NewSpeak has
been given a denotational semantics.

\subsubsection{SafeSpex}
(Specification and Verification of Safety Critical Systems).
The overall project objective is to investigate the relationship
between the tasks performed by safety engineers and software engineers
in order to achieve coherence between the theories employed. This
project has recently produced a rigorous methodology for deriving
software safety requirements from fault trees produced during hazard
analysis activities. The work
is done in collaboration with the safety critical systems group of the
Department of Computer Science at the Technical University of Denmark.
This project continues the lines of investigation established
within the ProCoS-1 project and is sponsored by the British Council.

\subsubsection{SafeFM}
The SafeFM (The practical application of formal methods to safety critical
systems) project is sponsored under the DTI/IED SafeIT programme. The
project aims to devise a methodology and calculus for constructing
provably coherent system specifications. It also aims to provide
guidelines on a cost effective approach to using formal methods in the
development and assessment of high integrity software systems. A
further aim is to develop models for the quantification of software.
The project team consists of the Safety and Reliability Directorate of
the UK Atomic Energy Authority, the Instruments Systems Division of
GEC Avionics and the Formal Methods Group of RHUL.

 
\subsubsection{DATUM}
The DATUM project (Dependability Assessment of Safety Critical Systems
 Through the Unification of Measurable Evidence) aims to advance the
state of the art in the 
 measurement and prediction of dependability, in particular safety.
The project is funded by the DTI/IED SafeIT programme and is a
collaboration between RHUL, the Centre for Software 
Reliability at City University, the
 Centre for Human Computer Interface Design at City University and the
 Performance Technology Group at Lloyds' Register. The FMG will
concentrate on research aiming to
 enable the incorporation of evidence from formal methods and HCI into
 judgments of system dependability.

\subsection{Connection Science and Machine Learning Group}

This group (Dr J Shawe-Taylor, Dr D A Cohen, Dr P G Jeavons, Mr Max
van Daalen and Mrs E Hogger) spans a number 
of projects ranging from the study and
implementation of Neural Networks to Computational Learning Theory and
Constraint Networks. The topics are mostly characterised by their
connectionist or distributed nature and many of the results relate to
the feasibility of learning such representations. 
There has been an enormous upsurge of interest in Neural Network models
of computation in recent years. The research undertaken at RHUL views
them in a wider context and is developing the theoretical foundations
which places the work on a firmer footing. 

\subsubsection{Computational Learning Theory}

Computational Learning Theory is the study of which classes of
functions can be inferred either from examples, queries or other
information. The theory has a firm mathematical foundation in
probability theory and provides invaluable insights into where the
difficulties in learning lie.  Our work has focused on estimations of
sample sizes needed for learning and application of these results to
connectionist learning paradigms. This allows for study of such elusive
properties as generalisation, as well as giving a framework for realistic 
assessments of learning algorithm performance. Both of these questions 
are crucial to large scale practical applications of Neural Networks. 

\subsubsection{Novel Digital Neural Chip}

Neural Networks offer the prospect of providing a standardised highly
parallel computation. Standard chips do not provide the
functionality required to perform the necessary operations, while
attempts to implement using analogue techniques require significant
development of fabrication and development methods.
We are currently developing a novel digital implementation of a
neural network chip. The initial theoretical and simulation results are
extremely promising.

\subsubsection{Neural Network Theory and Applications}

The study of the capabilities of neural networks and
their design to meet specific problem constraints.
We have developed a large scale simulation package
incorporating many of our theoretical ideas.
Solving NP-hard problems using neural techniques, in
particular the Mean Field Annealing algorithm and related
approaches.

\subsubsection{Constraint Networks}

One approach to the discovery of structure in data is to attempt to
model all the interacting constraints satisfied by the data.  This leads
to the investigation of networks of constraints which provides a
natural framework for the use of neural network models of computation.
We are investigating the capabilities of constraint networks for
representing data, the relationship to the relational model of
databases, and suitable learning algorithms. 

\subsubsection{Algorithmic Machine Learning}

We are exploring the use of algorithmic machine learning as a way of
discovering effective heuristics for the meta-level interpretation of
logic programs. This may lead to more efficient implementation strategies 
for large logic programs such as deductive databases. The learning algorithm 
used is expected to have wider application, for example in planning.

\subsection{ Information security}
Members of the Information Security Group are Professor C Mitchell, 
Dr D Gollmann, Dr S Murphy (joint appointment with the Department of 
Mathematics), and Professor F Piper, 
Dr P Wild and Dr M Burmester of the Mathematics Department. Current areas of 
research interest include: block ciphers, stream ciphers, unconditional authentication schemes,
digital signatures, cryptographic hash functions, and security in distributed systems.  
The group has a large number of post-graduate students, and continues to play 
host to many leading research experts through its international reputation.

The group has a number of very well-established industrial links, in 
particular with Vodafone Ltd., Racal Electronics Plc and Hewlett-Packard Ltd.  These links 
are based on a long running series of research seminars which have considerable
industrial participation and strong personal research collaborations with 
particular individuals such as Dr M Walker of Vodafone Ltd., who is Visiting 
Professor jointly at the Department of Mathematics and the Department of 
Computer Science. The department also has Donald Davies CBE FRS as a Visiting 
Professor, who is internationally known for his work in the field.

\subsubsection{Security Studies for Third Generation Mobile Telecommunications Systems}

This major new collaborative project, which started in
February 1993, is funded under the DTI/SERC LINK Personal
Communications Programme and involves
the RHUL Information Security Group, Vodafone and GPT.
SERC has funded one full-time post-doctoral research
assistant for the three year span of the project,
together with a half-time graduate RA for the same
period.

The project is intended to identify the security features
required for the third generation of mobile
telecommunications systems, likely to come into use early
in the next century.  Classes of security mechanisms
appropriate to provide the required features will be
identified.  The integration of these mechanisms into the
Intelligent Network architecture will also be considered.
The work on security mechanisms will be led by RHUL.

\subsubsection{Authentication protocols}

The group conducts research on the design, formal verification, and
implementation of authentication protocols for communication networks and
distributed systems. In this context, we examine how to provide consistent
clocks in a distributed system in a secure way. 
The research on authentication also serves as input to international
standardisation efforts through Professor Mitchell's contributions to the
work of ISO/IEC JTC1/SC27 on generic security mechanisms.

\subsection{Other research areas}

\subsubsection{Real Time Parallel Processing}

We are interested in highly parallel systems with predictable real-time 
response for applications in industrial control and vision. We are presently 
implementing a system which will offer computing power of up to 1GIP 
(1,000,000,000 instructions per second) at a cost of around \pounds10 per MIP. 
This project, lead by Dr A\,J\,C Johnstone,  receives substantial funding from 
SERC, the DTI and industry. 
Postgraduate work for the project centres around development of compilers and
code generators for the new machine. The main application of this system is in 
real-time vision systems, and we also have an interest in image processing and 
pattern recognition systems. We have substantial facilities for the
development of full and semi-custom VLSI chips, and welcome applications from 
candidates interested in VLSI architectures and CAD algorithms.

\subsubsection{Computational Analysis of Optical Propagation Phenomena}

In the field of signal propagation there is growing interest in being able 
to produce compact waveguide resonator devices.   

Investigations are being carried out by Mr A R Davies and Dr J Banerji in 
collaboration with The Defence Research Agency (RSRE,Malvern) on propagation 
phenomena in hollow dielectric folded waveguides. A computational model is 
being developed of multi--mode propagation devices of varying complexities 
based on combinations of beam splitter and recombiner structures. The model 
will be used to design and characterize the performances of optical devices 
including optical signal processors.
This work has been supported through successive stages of evolution and 
funded at varying levels through the MOD since 1972. 


\end{document}