Chris.Holt@newcastle.ac.uk (Chris Holt) (08/04/90)
[sorry if my cross-posting is inappropriate]
The University of Newcastle upon Tyne
Computing Laboratory
Temporary Research Associate
"Embedding Concurrent and Imperative Programming Constructs in
Interval Temporal Logic"
Information for Candidates
Applications are invited from suitably qualified graduates to work on an
SERC-sponsored project concerned with enhancing an implementation of an
interval temporal logic (ITL).
Temporal logic has become a popular formalism for specifying and
verifying concurrent programs, hardware and other dynamic systems.
One variant of temporal logic is called Interval Temporal Logic (ITL)
and as its name suggests, it is especially suited for reasoning about
periods of time. A programming language called Tempura has been
developed as an executable subset of ITL and used to simulate a number
of software and hardware examples. Tempura is one of the earliest
languages to be based on temporal logic.
In the present research project, we will augment ITL and Tempura to
directly embed conventional imperative programming constructs such
as assignments, loops and structured exits. This will enable us to
treat Pascal-like programs as ITL formulas. Existing temporal logics
do not have this capability.
We will also look at techniques for multi-level representation of
digital systems from the gate and machine language levels to the
programming language level. ITL's constructs enable us to uniformly
consider various levels of time granularity. General issues of
synchronous and asynchronous systems are also to be investigated.
Another part of the project consists of studying ITL's proof theory.
This includes the implementation of some decision procedures and
perhaps a verifier for suitable subsets of the logic.
Possible applications of ITL also include the specification of a
model digital railway.
Applicants should possess a good degree in computer science. Experience
with C and temporal logic would be advantageous.
The post is available immediately, and is initially funded for three
years. Salary will be at an appropriate point on the 1A Scale (11,399-
18,165), according to age, qualifications and experience. No forms of
application are issued, but applications giving full details of age,
qualifications, experience and present salary, together with the names
and addresses of three referees to whom reference may be made, should
be sent to Dr. C. M. Holt, Computing Laboratory, The University,
Newcastle upon Tyne, NE1 7RU, as quickly as possible, and not later
than 24th August 1990.
-----------------------------------------------------------------------------
Chris.Holt@newcastle.ac.uk Computing Lab, U of Newcastle upon Tyne, UK
-----------------------------------------------------------------------------
"Extreme bounds are most appropriate for extreme kangaroos..."