Limit of tenure: Three years
Ref: NR168
Salary: £19,460 - £29,127 per annum
Limit of tenure: One year
Ref: NR170
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:
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@cl.cam.ac.uk (e-mailed applications should be cc'd to Peter.Sewell@cl.cam.ac.uk).
Closing date: to be sure of full consideration, applications should arrive by 31 January 2005