| 2025 | ICFEM | Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks. | Kangfeng Ye, Roberto Metere, Jim Woodcock, Poonam Yadav |
| 2024 | ISoLA | Digital Twin Engineering. | John S. Fitzgerald, Cludio Gomes, Einar Broch Johnsen, Eduard Kamburjan, Martin Leucker, Jim Woodcock |
| 2023 | ICTAC | Modelling and Verifying Robotic Software that Uses Neural Networks. | Ziggy Attala, Ana Cavalcanti, Jim Woodcock |
| 2022 | ICFEM | Formally Verified Animation for RoboChart Using Interaction Trees. | Kangfeng Ye, Simon Foster, Jim Woodcock |
| 2022 | ISoLA | Engineering of Digital Twins for Cyber-Physical Systems. | John S. Fitzgerald, Peter Gorm Larsen, Tiziana Margaria, Jim Woodcock, Cludio Gomes |
| 2022 | ISoLA | Formally Verified Self-adaptation of an Incubator Digital Twin. | Thomas Wright, Cludio Gomes, Jim Woodcock |
| 2021 | CONCUR | Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL. | Simon Foster, Chung-Kil Hur, Jim Woodcock |
| 2021 | FMICS | Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps. | Simon Thrane Hansen, Cludio Gomes, Maurizio Palmieri, Casper Thule, Jaco van de Pol, Jim Woodcock |
| 2020 | ISoLA | Engineering of Digital Twins for Cyber-Physical Systems. | John S. Fitzgerald, Peter Gorm Larsen, Tiziana Margaria, Jim Woodcock |
| 2020 | ISoLA | Uncertainty Quantification and Runtime Monitoring Using Environment-Aware Digital Twins. | Jim Woodcock, Cludio Gomes, Hugo Daniel Macedo, Peter Gorm Larsen |
| 2020 | SETTA | Learning Safe Neural Network Controllers with Barrier Certificates. | Hengjun Zhao, Xia Zeng, Taolue Chen, Zhiming Liu, Jim Woodcock |
| 2018 | ISoLA | Cyber-Physical Systems Engineering: An Introduction. | J. Paul Gibson, Peter Gorm Larsen, Marc Pantel, John S. Fitzgerald, Jim Woodcock |
| 2017 | SEFM | Features of Integrated Model-Based Co-modelling and Co-simulation Technology. | Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock, Carl Gamble, Richard John Payne, Kenneth Pierce |
| 2016 | ICFEM | Checking SysML Models for Co-simulation. | Nuno Amlio, Richard John Payne, Ana Cavalcanti, Jim Woodcock |
| 2016 | ICTAC | Behavioural Models for FMI Co-simulations. | Ana Cavalcanti, Jim Woodcock, Nuno Amlio |
| 2016 | ICTAC | Unifying Heterogeneous State-Spaces with Lenses. | Simon Foster, Frank Zeyda, Jim Woodcock |
| 2016 | ISoLA | Towards Semantically Integrated Models and Tools for Cyber-Physical Systems Design. | Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock, Ren A. Nilsson, Carl Gamble, Simon Foster |
| 2016 | ISoLA | Heterogeneous Semantics and Unifying Theories. | Jim Woodcock, Simon Foster, Andrew Butterfield |
| 2015 | ICFEM | Refinement-Based Verification of the FreeRTOS Scheduler in VCC. | Sumesh Divakaran, Deepak D'Souza, Anirudh Kushwah, Prahladavaradan Sampath, Nigamanth Sridhar, Jim Woodcock |
| 2015 | ICSE | Cyber-Physical Systems Design: Formal Foundations, Methods and Integrated Tool Chains. | John S. Fitzgerald, Carl Gamble, Peter Gorm Larsen, Kenneth Pierce, Jim Woodcock |
| 2015 | ICTAC | CSP and Kripke Structures. | Ana Cavalcanti, Wen-ling Huang, Jan Peleska, Jim Woodcock |
| 2014 | FM | A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes. | Pedro R. G. Antonino, Augusto Sampaio, Jim Woodcock |
| 2014 | FM | Engineering UToPiA - Formal Semantics for CML. | Jim Woodcock |
| 2014 | ISoLA | Contracts in CML. | Jim Woodcock, Ana Cavalcanti, John S. Fitzgerald, Simon Foster, Peter Gorm Larsen |
| 2014 | SEFM | Rapid Prototyping of a Semantically Well Founded Circus Model Checker. | Alexandre Mota, Adalberto Farias, Andr Didier, Jim Woodcock |
| 2013 | ICTAC | Unifying Theories of Programming in Isabelle. | Simon Foster, Jim Woodcock |
| 2013 | SEFM | A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP. | Marcel Vincius Medeiros Oliveira, Ivan Soares de Medeiros Jnior, Jim Woodcock |
| 2011 | FM | The Safety-Critical Java Memory Model: A Formal Account. | Ana Cavalcanti, Andy J. Wellings, Jim Woodcock |
| 2011 | ICECCS | Using Model Transformation to Generate Graphical Counter-Examples for the Formal Analysis of xUML Models. | Osmar Marchi dos Santos, Jim Woodcock, Richard F. Paige |
| 2011 | ICECCS | Timed Circus: Timed CSP with the Miracle. | Kun Wei, Jim Woodcock, Alan Burns |
| 2010 | SEFM | A Timed Model of Circus with the Reactive Design Miracle. | Kun Wei, Jim Woodcock, Alan Burns |
| 2009 | ICST | Putting Formal Specifications under the Magnifying Glass: Model-based Testing for Validation. | Emine Gokce Aydal, Richard F. Paige, Mark Utting, Jim Woodcock |
| 2009 | TASE | State Visibility and Communication in Unifying Theories of Programming. | Andrew Butterfield, Pawel Gancarski, Jim Woodcock |
| 2008 | ICECCS | POSIX and the Verification Grand Challenge: A Roadmap. | Leo Freitas, Jim Woodcock, Andrew Butterfield |
| 2008 | ICECCS | Linking VDM and Z. | Jim Woodcock, Leo Freitas |
| 2008 | ICST | Observations for Assertion-based Scenarios in the context of Model Validation and Extension to Test Case Generation. | Emine Gokce Aydal, Richard F. Paige, Jim Woodcock |
| 2008 | ICTAC | A Theory of Pointers for the UTP. | Will Harwood, Ana Cavalcanti, Jim Woodcock |
| 2007 | ICECCS | Formalising Flash Memory: First Steps. | Andrew Butterfield, Jim Woodcock |
| 2007 | ICECCS | POSIX file store in Z/Eves: an experiment in the verified software repository. | Leo Freitas, Zheng Fu, Jim Woodcock |
| 2007 | ICECCS | Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository. | Leo Freitas, Konstantinos Mokos, Jim Woodcock |
| 2007 | ICFEM | Automatic Generation of Verified Concurrent Hardware. | Marcel Oliveira, Jim Woodcock |
| 2007 | ICFEM | A Denotational Semantics for Handel-C Hardware Compilation. | Juan Ignacio Perna, Jim Woodcock |
| 2007 | ICSoft | Goal-Oriented Automatic Test Case Generators for MC/DC Compliancy. | Emine Gokce Aydal, Jim Woodcock, Ana Cavalcanti |
| 2007 | IFM | Slotted-Circus. | Andrew Butterfield, Adnan Sherif, Jim Woodcock |
| 2007 | MODELS | Evaluation of OCL for Large-Scale Modelling: A Different View of the Mondex Purse. | Emine Gokce Aydal, Richard F. Paige, Jim Woodcock |
| 2006 | FM | Verified Software Grand Challenge. | Jim Woodcock |
| 2006 | ICECCS | A Layered Behavioural Model of Platelets. | Steve A. Schneider, Helen Treharne, Ana Cavalcanti, Jim Woodcock |
| 2006 | ICFEM | Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking. | Leo Freitas, Ana Cavalcanti, Jim Woodcock |
| 2006 | ICTAC | Z/Eves and the Mondex Electronic Purse. | Jim Woodcock, Leo Freitas |
| 2006 | SEW | First Steps in the Verified Software Grand Challenge. | Jim Woodcock |
| 2005 | FM | Operational Semantics for Model Checking Circus. | Jim Woodcock, Ana Cavalcanti, Leonardo Freitas |
| 2004 | IFM | A Tutorial Introduction to Designs in Unifying Theories of Programming. | Jim Woodcock, Ana Cavalcanti |
| 2004 | MPC | Travelling Processes. | Xinbei Tang, Jim Woodcock |
| 2004 | SEFM | Towards Mobile Processes in Unifying Theories. | Xinbei Tang, Jim Woodcock |
| 2003 | FM | A Circus Semantics for Ravenscar Protected Objects. | Diyaa-Addein Atiya, Steve King, Jim Woodcock |
| 2002 | FM | Refinement in Circus. | Augusto Sampaio, Jim Woodcock, Ana Cavalcanti |
| 2002 | ICFEM | Unifying Theories of Parallel Programming. | Jim Woodcock, Arthur P. Hughes |
| 2001 | APSEC | The Steam Boiler in a Unified Theory of Z and CSP. | Jim Woodcock, Ana Cavalcanti |
| 1999 | IFM | On the Refinement and Simulation of Data Types and Processes. | Christie Bolton, Jim Davies, Jim Woodcock |
| 1994 | ESORICS | Non-Interference Through Determinism. | A. W. Roscoe, Jim Woodcock, Lars Wulf |
| 1991 | FM | A Tutorial on the Refinement Calculus. | Jim Woodcock |
| 1991 | FM | The Refinement Calculus. | Jim Woodcock |
| 1991 | FM | An Introduction to Refinement in Z. | Jim Woodcock |
| 1991 | FM | Two Refinement Case Studies. | Jim Woodcock |
| 1990 | FM | Refinement of State-Based Concurrent Systems. | Jim Woodcock, Carroll Morgan |
| 1988 | FM | Using VDM with Rely and Guarantee-Conditions - Experiences from a Real Project. | Jim Woodcock, B. Dickinson |