[pept:7] Opening: Research Fellow in Model Checking and Program Analysis

[Michael Leuschel <mal@xxxxxxxxxxxxxxx>]

===================================================
Research Fellow
Model Checking and Program Analysis/Specialisation
===================================================

-----------------------------------------
Complete Information at:
http://www.ecs.soton.ac.uk/~mal/ISM.html
-----------------------------------------

Department of Electronics and Computer Science University of Southampton
Applications are invited for the above post at the Declarative Systems and
Software Engineering Research Group at Southampton.  The Department of
Electronics and Computer Science at the University of Southampton is the
largest department of its kind in the UK. It was awarded grade 5* for
Engineering and grade 5 for Computer Science in the 1996 national
assessment of research in UK Universities.

The fellowship is part of the EPSRC - funded project GR/N1166 researching
Infinite State Model Checking by Partial Evaluation and Abstract
Interpretation.  The past years have seen dramatic growth in the
application of model checking techniques to the validation and verification
of hardware systems.  However, despite the success of model checking, most
systems must be substantially simplified (i.e., abstracted) and
considerable human ingenuity is still required.  Furthermore, most software
systems cannot be modelled directly by a finite state system: as soon as
some kind of number recursion, dynamic or unbound data structures come into
play, an infinite number of states must be verified.

Job Description: The main objective of the project is to study the
potential of automatically deriving abstractions for infinite model
checking through a combination of existing technology for the automatic
control of partial evaluation and abstract interpretation.  First
successful experiments of this idea have been conducted using the ECCE and
LOGEN tools.  The project consists of a theoretical study coupled with the
implementation of a combined partial evaluation and abstract interpretation
system (based upon ECCE) The practicality of the approach will be gauged on
realistic examples, some of them coming from the EPSRC funded ABCD project
for the validation of business-critical systems.

The post is for 18 months.  Ideally the candidate should possess a PhD in
computer science and have experience of either model checking, logic
programming, partial evaluation or abstract interpretation.

Informal Enquiries may be made to Dr Michael Leuschel, Tel +44 (0)23 8059
3377, mal@ecs.soton.ac.uk

Salary range £16,286 to £24,479 per annum.

Application forms may be obtained from the Personnel Department (R),
University of Southampton, Highfield, Southampton, SO17 1BJ, Tel: 023 805
92750, e-mail: recruit@soton.ac.uk or minicom: 023 8059 5595.

To be returned no later than 23 February 2000.  Please quote reference
number R/343/WJ. Working for Equal Opportunities