Publications

Sort by: Date | Author | Title

Woodcock, J. (2025). Farewell Editorial. Formal Aspects of Computing, 37(4), Article 26. https://doi.org/10.1145/3773042

Wright, T., Dennis, L. A., Woodcock, J. & Foster, S. (2025). Formal Verification of BDI Agents. In M. Hinchey & B. Steffen (Eds.), The Combined Power of Research, Education, and Dissemination: Essays Dedicated to Tiziana Margaria on the Occasion of Her 60th Birthday (pp. 302-326). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-73887-6_20

Woodcock, J., Andersen, M. S., Aranha, D. F., Hallerstede, S., Hansen, S. T., Jakobsen, N. K., Kulik, T., Larsen, P. G., Macedo, H. D., Martin, C. I. I. & Norrild, V. A. M. (2023). State of the Art Report: Verified Computation. https://doi.org/10.48550/arXiv.2308.15191

Kulik, T., Dongol, B., Larsen, P. G., Macedo, H. D., Schnieder, S., Tran-Jørgensen, P. W. V. & Woodcock, J. (2022). A Survey of Practical Formal Methods for Security. Formal Aspects of Computing, 34(1), Article 3522582. https://doi.org/10.1145/3522582

Fitzgerald, J., Larsen, P. G., Margaria, T. & Woodcock, J. (2021). Engineering of Digital Twins for Cyber-Physical Systems. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings (pp. 49-53). Springer. https://doi.org/10.1007/978-3-030-83723-5_4

Woodcock, J., Gomes, C., Macedo, H. D. & Larsen, P. G. (2021). Uncertainty Quantification and Runtime Monitoring Using Environment-Aware Digital Twins. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings (pp. 72-87). Springer. https://doi.org/10.1007/978-3-030-83723-5_6

Foster, S., Ye, K., Cavalcanti, A. L. C. & Woodcock, J. (2020). Automated Verification of Reactive and Concurrent Programs by Calculation. ArXiv. https://eprints.whiterose.ac.uk/164020/1/2007.13529v1.pdf

Ye, K., Foster, S. D. & Woodcock, J. (2020). Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP. In A. Adamatzky & V. Kendon (Eds.), From Astrophysics to Unconventional Computation: Essays Presented to Susan Stepney on the Occasion of her 60th Birthday (pp. 215-254). Springer. https://doi.org/10.1007/978-3-030-15792-0_10

Chang, W., Wei, R., Zhao, S., Wellings, A., Woodcock, J. & Burns, A. (2020). Development Automation of Real-Time Java: Model-Driven Transformation and Synthesis. ACM Transactions on Embedded Computing Systems, 19(5), Article 3391897. https://doi.org/10.1145/3391897

Zhao, H., Zeng, X., Chen, T., Liu, Z. & Woodcock, J. (2020). Learning Safe Neural Network Controllers with Barrier Certificates. (pp. 177-185). ArXiv. https://doi.org/10.1007/978-3-030-62822-2_11

Foster, S. D., Baxter, J., Cavalcanti, A. L. C., Woodcock, J. & Zeyda, F. (2020). Unifying semantic foundations for automated verification tools in Isabelle/UTP. Science of Computer Programming, 197, Article 102510. https://doi.org/10.1016/j.scico.2020.102510

Foster, S. D., Cavalcanti, A. L. C., Canham, S. J., Woodcock, J. & Zeyda, F. (2020). Unifying theories of reactive design contracts. Theoretical Computer Science, 802, 105-140. https://doi.org/10.1016/j.tcs.2019.09.017

Hoare, T., Struth, G. & Woodcock, J. (2019). A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic. In P. Ribeiro & A. Sampaio (Eds.), Unifying Theories of Programming - 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Proceedings: 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Porto, Portugal, October 8, 2019, Proceedings (pp. 3-21). Springer. https://doi.org/10.1007/978-3-030-31038-7_1

Gleirscher, M., Foster, S. D. & Woodcock, J. (2019). New Opportunities for Integrated Formal Methods. ACM Computing Surveys, 52(6), 1-36. Article 117. https://doi.org/10.1145/3357231

Woodcock, J., Cavalcanti, A. L. C., Foster, S. D., Mota, A. & Ye, K. (2019). Probabilistic Semantics for RoboChart: A Weakest Completion Approach. In P. Ribeiro & A. Sampaio (Eds.), Unifying Theories of Programming - 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Proceedings: 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Porto, Portugal, October 8, 2019, Proceedings (pp. 80-105). Springer. https://doi.org/10.1007/978-3-030-31038-7_5

Heiji Miyazawa, A., De Oliveira Salazar Ribeiro, P. F., Li, W., Cavalcanti, A. L. C., Timmis, J. I. & Woodcock, J. (2019). RoboChart: modelling and verification of the functional behaviour of robotic applications. Software and Systems Modeling, 18(5), 3097–3149. https://doi.org/10.1007/s10270-018-00710-z

Conserva Filho, M. S., Marinho, R., Mota, A. & Woodcock, J. (2018). Analysing RoboChart with Probabilities. In T. Massoni & M. Reza Mousavi (Eds.), Formal Methods: Foundations and Applications - 21st Brazilian Symposium, SBMF 2018, Proceedings (pp. 198-214). Springer. https://doi.org/10.1007/978-3-030-03044-5_13

Foster, S. D., Baxter, J., Cavalcanti, A. L. C., Miyazawa, A. & Woodcock, J. (2018). Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. In K. Bae & P. Csaba Ölveczky (Eds.), Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings: 15th International Conference, FACS 2018, Pohang, South Korea, October 10–12, 2018, Proceedings (pp. 137-155). Springer. https://doi.org/10.1007/978-3-030-02146-7_7

Foster, S. D., Ye, K., Cavalcanti, A. L. C. & Woodcock, J. (2018). Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. In J. Desharnais, W. Guttmann & S. Joosten (Eds.), Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Proceedings: 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 – November 1, 2018, Proceedings (pp. 205-224). Springer. https://doi.org/10.1007/978-3-030-02149-8_13

Larsen, P. G., Fitzgerald, J., Woodcock, J., Gamble, C., Payne, R. & Pierce, K. (2018). Features of Integrated Model-Based Co-modelling and Co-simulation Technology. In A. Cerone & M. Roveri (Eds.), Software Engineering and Formal Methods - SEFM 2017 Collocated Workshops: DataMod, FAACS, MSE, CoSim-CPS, and FOCLASA, Revised Selected Papers (pp. 377-390). Springer. https://doi.org/10.1007/978-3-319-74781-1_26

Li, W., Miyazawa, A., Ribeiro, P., Cavalcanti, A. L. C., Woodcock, J. & Timmis, J. (2018). From Formalised State Machines to Implementations of Robotic Controllers. In Springer Proceedings in Advanced Robotics (pp. 517-529). Springer. https://doi.org/10.1007/978-3-319-73008-0_36

Foster, S. D., Cavalcanti, A. L. C., Woodcock, J. & Zeyda, F. (2018). Unifying theories of time with generalised reactive processes. Information Processing Letters, 135, 47-52. https://doi.org/10.1016/j.ipl.2018.02.017

Ribeiro, P., Cavalcanti, A. L. C. & Woodcock, J. (2017). A Stepwise Approach to Linking Theories. In J. P. Bowen & H. Zhu (Eds.), Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers (pp. 134-154). Springer. https://doi.org/10.1007/978-3-319-52228-9_7

Cavalcanti, A. L. C., Miyazawa, A., Payne, R. & Woodcock, J. (2017). Sound Simulation and Co-simulation for Robotics. In Present and Ulterior Software Engineering (pp. 173-194). Springer. https://doi.org/10.1007/978-3-319-67425-4_11

Foster, S. D. & Woodcock, J. (2017). Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL. In T. Gibson-Robinson, P. Hopcroft & R. Lazić (Eds.), Concurrency, Security, and Puzzles: Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday (pp. 39-64). Springer International Publishing. https://doi.org/10.1007/978-3-319-51046-0_3

Chapman, R., White, N. & Woodcock, J. (2017). What can agile methods bring to high-integrity software development? Communications of the A C M, 60(10), 38-41. https://doi.org/10.1145/3133233

Cavalcanti, A. L. C., Woodcock, J. & Amalio, N. (2016). Behavioural Models for FMI Co-simulations. In A. Sampaio & F. Wang (Eds.), Theoretical Aspects of Computing - ICTAC 2016, 13th International Colloquium, Proceedings: 13th International Colloquium, Taipei, Taiwan, ROC, October 24–31, 2016, Proceedings (pp. 255-273). Springer. https://doi.org/10.1007/978-3-319-46750-4_15

Amálio, N., Payne, R., Cavalcanti, A. L. C. & Woodcock, J. (2016). Checking SysML Models for Co-Simulation. In K. Ogata, M. Lawford & S. Liu (Eds.), Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Proceedings: 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings (pp. 450-465). Springer. https://doi.org/10.1007/978-3-319-47846-3_28

Woodcock, J., Foster, S. D. & Butterfield, A. (2016). Heterogeneous Semantics and Unifying Theories. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings (Vol. 1, pp. 374-394). Springer. https://doi.org/10.1007/978-3-319-47166-2_26

Larsen, P. G., Fitzgerald, J., Woodcock, J., Fritzson, P., Brauer, J., Kleijn, C., Lecomte, T., Pfeil, M., Green, O., Basagiannis, S. & Sadovykh, A. (2016). Integrated tool chain for model-based design of Cyber-Physical Systems: The INTO-CPS project. In 2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS (CPS Data) (pp. 1-6). IEEE. https://doi.org/10.1109/CPSData.2016.7496424

Woodcock, J., Wellings, A. & Cavalcanti, A. L. C. (2016). Mobile CSP. In M. Cornélio & B. Roscoe (Eds.), Formal Methods: Foundations and Applications - 18th Brazilian Symposium, SBMF 2015, Proceedings (pp. 39-55). Springer. https://doi.org/10.1007/978-3-319-29473-5_3

Larsen, P. G., Fitzgerald, J., Woodcock, J., Nilsson, R., Gamble, C. & Foster, S. (2016). Towards Semantically Integrated Models and Tools for Cyber-Physical Systems Design. In M. Tiziana & S. Bernhard (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Proceedings (Vol. II, pp. 171-186). Springer. https://doi.org/10.1007/978-3-319-47169-3_13

Foster, S. D., Zeyda, F. & Woodcock, J. (2016). Unifying Heterogeneous State-Spaces with Lenses. In A. Sampaio & F. Wang (Eds.), Theoretical Aspects of Computing - ICTAC 2016, 13th International Colloquium, Proceedings: 13th International Colloquium, Taipei, Taiwan, ROC, October 24–31, 2016, Proceedings (pp. 295-314). Springer. https://doi.org/10.1007/978-3-319-46750-4_17

Martin, A. P., Gardiner , P. H. B. & Woodcock, J. (2015). A tactic calculus — abridged version. Formal Aspects of Computing, 8, 479–489 . https://doi.org/10.1007/BF01213535

Fitzgerald, J., Gamble, C., Larsen, P. G., Pierce, K. & Woodcock, J. (2015). Cyber-Physical Systems Design: Formal Foundations, Methods and Integrated Tool Chains. In Proceedings of the 2015 IEEE/ACM 3rd FME Workshop on Formal Methods in Software Engineering (FormaliSE) (pp. 40-46). IEEE. https://doi.org/10.1109/FormaliSE.2015.14

Sinclair, J. & Woodcock, J. (2015). Event refinement in state-based concurrent systems. Formal Aspects of Computing, 7, 266–288. https://doi.org/10.1007/BF01211074

Mota, A., Farias, A., Woodcock, J. & Larsen, P. G. (2015). Model checking CML : tool development and industrial applications. Formal Aspects of Computing, 5(27), 975–1001. https://doi.org/10.1007/s00165-015-0342-2

Ye, K. & Woodcock, J. (2015). Model checking of state-rich formalism by linking to CSP∥B. International Journal on Software Tools for Technology Transfer, 19(1), 73–96. https://doi.org/10.1007/s10009-015-0402-1

Divakaran, S., D’Souza, D., Kushwah, A., Sampath, P., Sridhar, N. & Woodcock, J. (2015). Refinement-Based Verification of the FreeRTOS Scheduler in VCC. In M. Butler, S. Conchon & F. Zaïdi (Eds.), Formal Methods and Software Engineering: 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings (pp. 170-186). Springer. https://doi.org/10.1007/978-3-319-25423-4_11

Nielsen, C. B., Larsen, P. G., Fitzgerald, J., Woodcock, J. & Peleska, J. (2015). Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions. A C M Computing Surveys, 48(2). https://doi.org/10.1145/2794381

Canham, S. J. & Woodcock, J. (2015). Three Approaches to Timed External Choice in UTP. In D. Naumann (Ed.), Unifying Theories of Programming: 5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers (pp. 1-20). Springer. https://doi.org/10.1007/978-3-319-14806-9_1

Wei, K. & Woodcock, J. (2015). Towards Algebraic Semantics of Circus Time. In D. Naumann (Ed.), Unifying Theories of Programming: 5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers (pp. 84-104). Springer. https://doi.org/10.1007/978-3-319-14806-9_5

Foster, S. D., Miyazawa, A., Woodcock, J., Cavalcanti, A. L. C., Fitzgerald, J. & Larsen, P. G. (2014). An approach for managing semantic heterogeneity in Systems of Systems Engineering. In S. Cook, V. Ireland, A. Gorod, T. Ferris & Q. Do (Eds.), John Fitzgerald (pp. 113-118). IEEE. https://doi.org/10.1109/SYSOSE.2014.6892473

Antonino, P., Sampaio, A. & Woodcock, J. (2014). A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes. In C. Jones, P. Pihlajasaari & J. Sun (Eds.), FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12-16, 2014. Proceedings (pp. 62-77). Springer. https://doi.org/10.1007/978-3-319-06410-9_5

Woodcock, J., Cavalcanti, A., Fitzgerald, J., Foster, S. & Larsen, P. G. (2014). Contracts in CML. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications: 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part II (pp. 54-73). Springer. https://doi.org/10.1007/978-3-662-45231-8_5

Woodcock, J. (2014). Engineering UToPiA: Formal Semantics for CML. In C. Jones, P. Pihlajasaari & J. Sun (Eds.), FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12-16, 2014. Proceedings (pp. 22-41). Springer. https://doi.org/10.1007/978-3-319-06410-9_3

Mota, A., Farias, A., Didier, A. & Woodcock, J. (2014). Rapid Prototyping of a Semantically Well Founded Circus Model Checker. In D. Giannakopoulou & G. Salaün (Eds.), Software Engineering and Formal Methods (pp. 235-249). Springer. https://doi.org/10.1007/978-3-319-10431-7_17

Medeiros Oliveira, M. V., Soares De Medeiros Júnior, I. & Woodcock, J. (2013). A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP. In R. M. Hierons, M. G. Merayo & M. Bravetti (Eds.), Software Engineering and Formal Methods: 11th International Conference, SEFM 2013, Madrid, Spain, September 25-27, 2013. Proceedings (pp. 46-60). Springer. https://doi.org/10.1007/978-3-642-40561-7_4

Fitzgerald, J., Larsen, P. G. & Woodcock, J. (2013). Foundations for Model-based Engineering for Systems of Systems. In M. Aiguier, F. Boulanger, D. Krob & C. Marchal (Eds.), Complex Systems Design & Management : Proceedings of the Fourth International Conference on Complex Systems Design & Management CSD&M 2013 (pp. 1-19). Springer VS. https://doi.org/10.1007/978-3-319-02812-5_1

Wei, K., Woodcock, J. & Burns, A. (2013). Modelling temporal behaviour in complex systems with Timebands. Formal Methods in System Design, 3(43), 520–551. https://doi.org/10.1007/s10703-013-0193-5

Displaying results 1 to 50 out of 161

Revised 13.11.2025

James Woodcock