Jim Woodcock's research page

Current research interests

Jim Woodcock's photo I am Professor of Software Engineering at the University of York, known for my research, teaching, and consultancy on the application of industrial-scale software engineering and formal methods.

Research method

Elucidation of sound mathematical principles underlying the practice of software engineering, using a research method based on interactions between abstract theory, pilot development, industrial collaboration, consultancy, tool development, and practical evaluation.

Research projects

I am currently an investigator on the following research projects:

  • INTO-CPS Integrated Tool Chain for Model-based Design of Cyber-Physical Systems, European Commission January 2015–December 2017
  • RoboCalc A Calculus for Software Engineering of Mobile and Autonomous Robots, EPSRC September 2015– August 2020, (PI: Professor A. Cavalcanti)
  • Software Engineering for Mobile Autonomous Robots, Royal Academy of Engineering June 2016– July 2017
  • Business innovation through digital technology, Visiting Professorship (D. Whittington), Royal Academy of Engineering March 2015–March 2018
  • Test-generation for mobile and autonomous robot controllers, Distinguished Visiting Fellowship (A. Sampaio), Royal Academy of Engineering June–July 2016
  • Indian Newton project

Graduate Students

  • Pakorn Waewsawangwong. PhD student, University of York. In progress (due 2017).
  • Samuel Canham. PhD student, University of York. In progress (due 2016).
  • Kangfeng Ye (Randall). Model Checking of State-Rich Formalisms (By Linking to Combination of State-based Formalism and Process Algebra). PhD student, University of York. Submitted 2016.
  • Gerard Ekembe Ngondi. Denotational Semantics of Mobility in Unifying Theories of Programming (UTP). PhD student, University of York. Submitted 2016.
  • Victor Bandur, Unifying Theories of Multi-Valued Logic. PhD student, University of York. Submitted 2016.
  • Shu Cheng. Formal Modelling and Verifying the Real-time Operating System. PhD, University of York. 2016.
  • Marcel Oliveira. A Refinement Calculus for Circus. PhD (jointly supervised with Ana Cavalcanti), University of York. 2006.
  • Juan Ignacio Perna. A Verified Compiler for Handel-C. PhD, University of York. 2010.
  • Emine Aydal. Model-Based Robustness Testing of Black Box Systems. University of York. 2006.
  • Alistair McEwan. Concurrent Program Development in Circus. DPhil student, Oxford University. 2006.
  • Leonardo Freitas. Model Checking Circus. PhD (jointly supervised with Ana Cavalcanti), University of York. 2005.
  • Andrew Simpson. Safety through Security. DPhil thesis, Oxford University & Smith Institute for Industrial Mathematics and Systems Engineering. 1996. Recommended for the 1997 Distinguished Dissertation Award of the CPHC.
  • Ana Cavalcanti. The Theory and Practice of Refinement in Z. DPhil, Oxford University. 1997.
  • Andrew Martin. Machine-Assisted Theorem Proving for Software Engineering. DPhil, Oxford University. 1994.
  • Jim Davies. Specification and Proof in Real-Time Systems. DPhil thesis, Oxford University. 1991. Winner of the 1992 Distinguished Dissertation Award of the Conference of Professors and Heads of Computing (CPHC).
  • Azadeh Shafibegly. Improving Software. PhD (jointly supervised with Agnes Kaposi), GEC Research Laboratories & Polytechnic of the South Bank. 1984.

Keynote speeches 2006–present

  • Engineering UToPiA—Formal Semantics for CML. FM Singapore 2014
  • Contracts in CML. ISoLA Corfu 2014
  • Unifying Theories of Programming in Isabelle. ICTAC Singapore 2013
  • Simulink Timed Models for Program Verification. Theories of Programming and Formal Methods. Shanghai 2013
  • Unifying Theories of Undefinedness in UTP. UTP Paris 2012
  • Modelling and Implementing Complex Systems with Timebands. SSIRI Singapore 2010
  • The Miracle of Reactive Programming. UTP Dublin 2008
  • POSIX and the Verification Grand Challenge: A Roadmap. ICECCS Belfast 2008
  • Formalising Flash Memory: First Steps. ICECCS Auckland 2007
  • Z/Eves and the Mondex Electronic Purse. ICTAC Tunisia 2006
  • Verified Software Grand Challenge. FM Canada 2006
  • First Steps in the Verified Software Grand Challenge. SEW NASA Langley 2006



© 10 August 2016