[TYPES] Research positions in Network Semantics, University of Cambridge

[Peter Sewell]

[our apologies for multiple copies]

NETSEM: Rigorous Semantics for Real Systems
Research Associate and Research Assistant positions
<http://www.cl.cam.ac.uk/users/pes20/Netsem/advert.html>

Computer Laboratory, University of Cambridge


Research Associate (post-doctoral)
Limit of tenure: Three years
Salary: 19,460 - 29,127 per annum

Research Assistant (post-graduate)
Limit of tenure: One year
Salary: 19,460 - 21,640 per annum

Two research positions are available on EPSRC grant EP/C510712 to
develop and apply rigorous semantic techniques to real-world network
systems. The investigators are Peter Sewell, Keith Wansbrough, and
Richard Gibbens, of the Computer Laboratory, University of Cambridge,
in collaboration with Michael Norrish, of NICTA, Canberra. The group
has recently developed a post-hoc behavioural specification of TCP,
UDP, and the Sockets API, expressed in the higher-order logic of the
HOL theorem proving system. It has been experimentally validated
against the behaviour of deployed implementations by novel HOL
symbolic model checking techniques. We aim now to build on this work
in various ways, improving the techniques, developing simpler
higher-level specifications, reasoning about algorithms implemented
above the Sockets API, and applying the techniques to new protocols.

For the Research Associate position you should have a PhD in Computer
Science or relevant Mathematics, ideally with experience in automated
reasoning, networking, and/or operational semantics. For the Research
Assistant position you should have a first-class degree in Computer
Science; this position would be appropriate for someone thinking of
going on to do a PhD. For either, an interest in addressing realistic
systems with mathematical rigour is essential. The starting date would
be 1 March 2005 or, subject to mutual agreement, up to 6 months
thereafter. Enquiries about the project should be addressed to Dr
Peter Sewell (http://www.cl.cam.ac.uk/~pes20), from whom further
details are available.

Applications should include:

  * a Curriculum Vitae
  * a completed form PD18 (from
     http://www.admin.cam.ac.uk/offices/personnel/forms/pd18/)
  * the names and e-mail addresses of two referees
  * a brief statement (up to one page) of your research interests
     and the particular contribution you would make to the project

Applications should be e-mailed (in postscript or pdf format,
printable on A4 paper) or sent to Kate Ellis, Computer Laboratory,
William Gates Building, JJ Thomson Avenue, Cambridge CB3 0FD,
UK. E-mail: Kate.Ellis at cl.cam.ac.uk (e-mailed applications should be
cc'd to Peter.Sewell at cl.cam.ac.uk).

Closing date: to be sure of full consideration, applications should
arrive by 31 January 2005