Bill Roscoe - Short Biography#

Bill Roscoe (Andrew William, hence A.W. Roscoe on papers) was born and brought up in Dundee, Scotland. He read Mathematics at University College, Oxford (Univ) 1975-78, obtaining the top mark for his year in the university. Together with another Univ student, Steve Brookes (now at CMU), he joined the Computing Laboratory (PRG) as a research student in 1978, and their DPhil work with Tony Hoare was on the mathematical foundations and models of his Communicating Sequential Processes (CSP) process algebra. Almost all Bill's subsequent research has either been based on CSP or has been a spin-off from it (examples of the latter being Hardware Verification and Computer Security). He was a Junior Research Fellow of St Edmund Hall 1980-3 and a Royal Society Research Fellow 1982-3. He became a College Lecturer at Univ in 1979 and a Tutorial Fellow there in 1983, when he was also appointed a University Lecturer in Computer Science at Oxford. He was given the title of Professor in 1997. In 2007 his job title was changed to "Research Professor" and he became a Senior Research Fellow at Univ. In 1993-7 he was Senior Tutor of Univ, in 1998-2000 he was the last ever Chairman of the Mathematical Sciences Faculty Board, and is Director of OUCL (now Department of Computer Science) 2003-8 and 2009-14.

Positions and activities:

• Chairman, Mathematical Sciences Faculty Board, Oxford, 1998-2000
• Head of Department, Oxford University Computing Laboratory 2003- : led major enlargement and broadening of department, which is rated number 1 in Europe by ARWU.
• Editor of Formal Methods in System Design
• 5 published collections of papers

Organised conferences:

• Pittsburgh seminar on concurrency 1984
• MFPS 1992 and 2009
• AVoCS 2007
• Retirement conference and 75th birthday events for Hoare, 1999 and 2009

Supervision

Over 50 successful doctoral descendants in all: those marked * below have had doctoral students themselves. 23 doctorates to completion.

• 1985 T.Y. Kong* Digital Topology
• 1986 A. Boucher Real-time semantics for occam
• 1988 G.M. Reed* Timed CSP
• 1989 M. Ward* Program Transformation
• 1989 Naiem Dathi Deadlock
• 1989 G. Barrett Operational semantics of the transputer
• 1991 A. Jeffrey* Timed Concurrency
• 1993 G. Lowe* Priority and Probability in Timed CSP
• 1995 B.G.O. Scott Semantics of occam II and its applications
• 1996 L. Wulf Refinement and security modelling in CSP
• 1998 J.B. Scattergood Tools for CSP (part-time doctorate)
• 1999 R.S. Lazic* Set Theory/Data independence
• 1999 R. Forster Foundations of Computer Security
• 2001 S.J. Creese* Inductive proofs of networks
• 2002 P.J. Broadfoot Proofs of cryptoprotocol security
• 2003 T. Newcomb Data independence
• 2006 R. Tolcher Ethnomethodology
• 2007 L. Momtahan Data independence in model generation
• 2008 E. Kleiner Web Services Security
• 2009 L.H. Nguyen New generation cryptoprotocols
• 2010 Huang Jian Timed theory of information flow
• 2011 N. Moffat Exploiting symmetry in model checking (part time)
• 2011 R. Kainda Human factors in security protocols

Major industrial collaborations include inmos, Qinetiq, Verum (start-up company embedding FDR in its product).

Over £4M research funding from EPSRC, EU, US Navy, and industry.

24 Invited talks listed on CV, including SPIN, CAV, Concur, MFPS