Jim Woodcock's research
Current research interests
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.
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
I am currently an
investigator on the following research projects:
Integrated Tool Chain for Model-based Design of
Cyber-Physical Systems, European Commission January
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
- Test-generation for
mobile and autonomous robot controllers, Distinguished
Visiting Fellowship (A. Sampaio), Royal Academy of
Engineering June–July 2016
- Indian Newton project
- 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
- 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
- Emine Aydal. Model-Based
Robustness Testing of Black Box Systems. University of
- Alistair McEwan. Concurrent
Program Development in Circus. DPhil student, Oxford
- 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
- 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
Keynote speeches 2006–present
UToPiA—Formal Semantics for CML. FM Singapore 2014
- Contracts in CML. ISoLA
- 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
- The Miracle of Reactive
Programming. UTP Dublin 2008
- POSIX and the
Verification Grand Challenge: A Roadmap. ICECCS
- 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