Publications

Sort by: Date | Author | Title

Freitas, L., Woodcock, J. & Butterfield, A. (2008). POSIX and the Verification Grand Challenge: A Roadmap. In K. Breitman, J. Woodcock, R. Sterritt & M. G. Hinchey (Eds.), ICECCS 2008: THIRTEENTH IEEE INTERNATIONAL CONFERENCE ON THE ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS (pp. 153-162). IEEE Computer Society Press. https://doi.org/10.1109/ICECCS.2008.35

Freitas, L. & Woodcock, J. (2007). FDR Explorer. Electronic Notes in Theoretical Computer Science, 187, 19-34. https://doi.org/10.1016/j.entcs.2006.08.042

Freitas, L., Fu, Z. & Woodcock, J. (2007). POSIX file store in Z/Eves: an experiment in the verified software repository. In 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007) (pp. 3-14). IEEE. https://doi.org/10.1109/ICECCS.2007.36

Freitas, L., Mokos, K. & Woodcock, J. (2007). Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository. In 2007 IEEE International Conference on Engineering of Complex Computer Systems (Vol. 1, pp. 290-298). IEEE. https://doi.org/10.1109/ICECCS.2007.45

Freitas, L., Woodcock, J. & Cavalcanti, A. L. C. (2006). State-rich model checking. Innovations in Systems and Software Engineering, 2, 49–64. https://doi.org/10.1007/s11334-006-0021-9

Freitas, L., Cavalcanti, A. L. C. & Woodcock, J. (2006). Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking. In Z. Liu & J. He (Eds.), Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006. Proceedings (pp. 697-716). Springer. https://doi.org/10.1007/11901433_38

Freeman Paige, R., Brooke, P. J., Song Dong, J. & Woodcock, J. (2009). Editorial. Formal Aspects of Computing, 21(4). https://doi.org/10.1007/s00165-009-0113-z

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

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

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

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., 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

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

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

Foster, S. D. & Woodcock, J. (2013). Unifying Theories of Programming in Isabelle. In Z. Liu, J. Woodcock & H. Zhu (Eds.), Unifying Theories of Programming and Formal Engineering Methods: International Training School on Software Engineering, Held at ICTAC 2013, Shanghai, China, August 26-30, 2013, Advanced Lectures (Vol. 1, pp. 109-155). Springer Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39721-9

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

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

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

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

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

Derrick, J., A. Boiten, E., Woodcock, J. & von Wright, J. (2002). Preface: Volume 70, Issue 3. Electronic Notes in Theoretical Computer Science, 70(3), 1-2. https://doi.org/10.1016/S1571-0661(05)80478-5

Cooper, D., Stepney, S. & Woodcock, J. (2002). Derivation of Z Refinement Proof Rules: Forwards and backwards rules incorporating input/output refinement. University of York. https://www-users.cs.york.ac.uk/~susan/bib/ss/z/347.pdf

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

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

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

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

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

Cavalcanti, A. L. C., Zeyda, F., Wellings, A., Woodcock, J. & Wei, K. (2013). Safety-critical Java programs from Circus models. Real-Time systems, 5(49), 614–667. https://doi.org/10.1007/s11241-013-9182-4

Cavalcanti, A. L. C., Wellings, A., Woodcock, J., Wei, K. & Zeyda, F. (2011). Safety-critical Java in Circus. In 9th Workshop on Java Technologies for Real-Time and Embedded System (pp. 20–29) https://doi.org/10.1145/2043910.2043915

Cavalcanti, A. L. C., Wellings, A. & Woodcock, J. (2011). The Safety-Critical Java Memory Model: A Formal Account. In M. Butler & W. Schulte (Eds.), FM 2011: Formal Methods (Vol. 1, pp. 246-261). Springer. https://doi.org/10.1007/978-3-642-21437-0

Cavalcanti, A. L. C., Woodcock, J. & Dunne, S. (2006). Angelic nondeterminism in the unifying theories of programming. Formal Aspects of Computing, 18(3), 288–307 . https://doi.org/10.1007/s00165-006-0001-8

Cavalcanti, A. L. C., Harwood, W. & Woodcock, J. (2006). Pointers and Records in the Unifying Theories of Programming. In S. Dunne & B. Stoddart (Eds.), Unifying Theories of Programming: First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006, Revised Selected Papers (pp. 200-216). Springer. https://doi.org/10.1007/11768173_12

Cavalcanti, A. L. C., Sampaio, A. & Woodcock, J. (2005). Unifying classes and processes. Software and Systems Modeling, 4, 277–296. https://doi.org/10.1007/s10270-005-0085-2

Cavalcanti, A. L. C. & Woodcock, J. (2005). Angelic Nondeterminism and Unifying Theories of Programming. Electronic Notes in Theoretical Computer Science, 137(2), 45-66. https://doi.org/10.1016/j.entcs.2005.04.024

Cavalcanti, A. L. C., Sampaio, A. & Woodcock, J. (2003). A Refinement Strategy for Circus. Formal Aspects of Computing, 15, 146–181. https://doi.org/10.1007/s00165-003-0006-5

Cavalcanti, A. L. C. & Woodcock, J. (2003). Predicate transformers in the semantics of Circus. IEE Proceedings - Software, 2(150). https://doi.org/10.1049/ip-sen:20030131

Cavalcanti, A. L. C., Sampaio, A. & Woodcock, J. (2002). Refinement of Actions in Circus. Electronic Notes in Theoretical Computer Science, 70(3), 132-162. https://doi.org/10.1016/S1571-0661(05)80489-X

Cavalcanti, A. L. C., Sampaio, A. & Woodcock, J. (1999). An Inconsistency in Procedures, Parameters and Substitution in the Refinement Calculus. Science of Computer Programming, 33, 87-96 . https://core.ac.uk/download/pdf/82142214.pdf

Cavalcanti, A. L. C. & Woodcock, J. (1998). A Weakest Precondition Semantics for Z. The Computer Journal, 41(1), 1-15. https://doi.org/10.1093/comjnl/41.1.1

Cavalcanti, A. L. C., Sampaio, A. & Woodcock, J. (1998). Procedures and Recursion in the Refinement Calculus. Journal of the Brazilian Computer Society , 5(1). https://doi.org/10.1590/S0104-65001998000200002

Cavalcanti, A. L. C. & Woodcock, J. (2005). ZRC – A Refinement Calculus for Z. Formal Aspects of Computing, 10, 267–289. https://doi.org/10.1007/s001650050016

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

Butterfield, A., Freitas, L. & Woodcock, J. (2008). Mechanising a formal model of flash memory. Science of Computer Programming, 74(4), 219-237. https://doi.org/10.1016/j.scico.2008.09.014

Butterfield, A., Gancarski, P. & Woodcock, J. (2009). State Visibility and Communication in Unifying Theories of Programming. In 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering IEEE. https://doi.org/10.1109/TASE.2009.57

Butterfield, A. & Woodcock, J. (2007). Formalising Flash Memory: First Steps. In 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007) IEEE. https://doi.org/10.1109/ICECCS.2007.23

Butterfield, A., Sherif, A. & Woodcock, J. (2007). Slotted-Circus: A UTP-Family of Reactive Theories. In J. Davies & J. Gibbons (Eds.), Integrated Formal Methods: 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007. Proceedings (pp. 75-97). Springer. https://doi.org/10.1007/978-3-540-73210-5_5

Butterfield, A. & Woodcock, J. (2006). A “Hardware Compiler” Semantics for Handel-C. Electronic Notes in Theoretical Computer Science, 161, 73-90. https://doi.org/10.1016/j.entcs.2006.04.026

Butterfield, A. & Woodcock, J. (2005). prialt in Handel-C: an operational semantics. International Journal on Software Tools for Technology Transfer, 7, 248–267. https://doi.org/10.1007/s10009-004-0181-6

Butterfield, A. & Woodcock, J. (2003). An Operational Semantics for Handel-C. Electronic Notes in Theoretical Computer Science, 80, 235-250. https://doi.org/10.1016/S1571-0661(04)80821-1

Displaying results 101 to 150 out of 161

Revised 13.11.2025

James Woodcock