Publications

Sort by: Date | Author | Title

Sampaio, A., Woodcock, J. & Cavalcanti, A. L. C. (2002). Refinement in Circus. In L.-H. Eriksson & P. A. Lindsay (Eds.), FME 2002:Formal Methods—Getting IT Right: International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22–24, 2002 Proceedings (pp. 451-470). Springer. https://doi.org/10.1007/3-540-45614-7_26

Roscoe, A. W., Woodcock, J. & Wulf, L. (1996). Non-interference through Determinism. Journal of Computer Security, 4(1), 27-53. https://doi.org/10.3233/JCS-1996-4103

Roscoe, A. W., Woodcock, J. & Wulf, L. (2005). Non-interference through determinism. In D. Gollmann (Ed.), Computer Security — ESORICS 94: Third European Symposium on Research in Computer Security Brighton, United Kingdom, November 7–9, 1994 Proceedings (pp. 31-53). Springer. https://doi.org/10.1007/3-540-58618-0_55

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

Radjenovic, A., Freeman Paige, R., Rose, L., Woodcock, J. & King, S. (2012). A Plug-in Based Approach for UML Model Simulation. In A. Vallecillo, J.-P. Tolvanen, E. Kindler, H. Störrle & D. Kolovos (Eds.), Modelling Foundations and Applications: 8th European Conference, ECMFA 2012, Kgs. Lyngby, Denmark, July 2-5, 2012. Proceedings (Vol. 1, pp. 328-339). Springer Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31491-9

Perna, J. I. & Woodcock, J. (2009). Mechanised Wire-wise Verification of Handel-C Synthesis. Electronic Notes in Theoretical Computer Science, 240, 201-219. https://doi.org/10.1016/j.entcs.2009.05.053

Perna, J. I. & Woodcock, J. (2008). UTP Semantics for Handel-C. In A. Butterfield (Ed.), Unifying Theories of Programming: Second International Symposium, UTP 2008, Dublin, Ireland, September 8-10, 2008, Revised Selected Papers (pp. 142-160). Springer. https://doi.org/10.1007/978-3-642-14521-6_9

Perna, J. I. & Woodcock, J. (2007). A Denotational Semantics for Handel-C Hardware Compilation. In M. Butler, M. G. Hinchey & M. M. Larrondo-Petrie (Eds.), Formal Methods and Software Engineering: 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007. Proceedings (pp. 266-285). Springer. https://doi.org/10.1007/978-3-540-76650-6_16

Oliveira, M., Cavalcanti, A. L. C. & Woodcock, J. (2007). A UTP semantics for Circus. Formal Aspects of Computing, 21, 3–32. https://doi.org/10.1007/s00165-007-0052-5

Oliveira, M., Cavalcanti, A. L. C. & Woodcock, J. (2007). A Denotational Semantics for Circus. Electronic Notes in Theoretical Computer Science, 187, 107-123. https://doi.org/10.1016/j.entcs.2006.08.047

Oliveira, M. & Woodcock, J. (2007). Automatic Generation of Verified Concurrent Hardware. In M. Butler, M. G. Hinchey & M. M. Larrondo-Petrie (Eds.), Formal Methods and Software Engineering: 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007. Proceedings (pp. 286-306). Springer. https://doi.org/10.1007/978-3-540-76650-6_17

Oliveira, M., Cavalcanti, A. L. C. & Woodcock, J. (2006). Unifying Theories in ProofPower-Z. 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. 123-140). Springer. https://doi.org/10.1007/11768173_8

Oliveira, M., Cavalcanti, A. L. C. & Woodcock, J. (2005). Formal development of industrial-scale systems in Circus. Innovations in Systems and Software Engineering, 1, 125–146 . https://doi.org/10.1007/s11334-005-0014-0

Oliveira, M., Cavalcanti, A. L. C. & Woodcock, J. (2003). ArcAngel: a Tactic Language for Refinement. Formal Aspects of Computing, 15, 28–47. https://doi.org/10.1007/s00165-003-0003-8

Nuka, G. & Woodcock, J. (2006). Mechanising a Unifying Theory. 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. 217-235). Springer. https://doi.org/10.1007/11768173_13

Nuka, G. & Woodcock, J. (2004). Mechanising the Alphabetised Relational Calculus. Electronic Notes in Theoretical Computer Science, 95, 209-225. https://doi.org/10.1016/j.entcs.2004.04.013

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

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

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

Meyer, B. & Woodcock, J. (Eds.) (2005). Verified Software: Theories, Tools, Experiments: First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions. In B. Meyer & J. Woodcock (Eds.), Verified Software: Theories, Tools, Experiments: First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions (Vol. 1). Springer. https://doi.org/10.1007/978-3-540-69149-5

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

M. dos Santos, O., Woodcock, J. & Freeman Paige, R. (2011). Using Model Transformation to Generate Graphical Counter-Examples for the Formal Analysis of xUML Models. In 2011 16th IEEE International Conference on Engineering of Complex Computer Systems (pp. 117-126). IEEE. https://doi.org/10.1109/ICECCS.2011.19

M. dos Santos, O., Woodcock, J., Freeman Paige, R. & King, S. (2009). The Use of Model Transformation in the INESS Project. In F. S. de Boer, M. M. Bonsangue, S. Hallerstede & M. Leuschel (Eds.), Formal Methods for Components and Objects: 8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers (Vol. 1, pp. 147-165). Springer. https://doi.org/10.1007/978-3-642-17071-3

McEwan, A. A. & Woodcock, J. (2008). Unifying Theories of Interrupts. In A. Butterfield (Ed.), Unifying Theories of Programming: Second International Symposium, UTP 2008, Dublin, Ireland, September 8-10, 2008, Revised Selected Papers (pp. 122-141). Springer. https://doi.org/10.1007/978-3-642-14521-6_8

McEwan, A. A. & Woodcock, J. (2004). A REFINEMENT BASED APPROACH TO CALCULATING A FAULT-TOLERANT RAILWAY SIGNAL DEVICE. In 18th World Computer Congress Topical Sessions (pp. 621-627). Springer. https://www.readcube.com/articles/10.1007%2F978-1-4020-8157-6_60

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

Liu, Z. & Woodcock, J. (2011). Editorial. Formal Aspects of Computing, 23(2), 151. https://doi.org/10.1007/s00165-011-0173-8

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

Larsen, P. G. & Woodcock, J. (Eds.) (1993). FME'93: Industrial-Strength Formal Methods : First International Symposium of Formal Methods Europe Proceedings, 19-23 April 1993, Odense, Denmark. Springer. Lecture Notes in Computer Science Vol. 670

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

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

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

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

Jones, C. B. & Woodcock, J. (2007). Editorial. Formal Aspects of Computing, 20(1), 1-3. https://doi.org/10.1007/s00165-007-0064-1

Jones, C. & Woodcock, J. (2007). Editorial. Formal Aspects of Computing, 19(4), 415–416. https://doi.org/10.1007/s00165-007-0046-3

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

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

Harwood, W., Cavalcanti, A. L. C. & Woodcock, J. (2008). A Theory of Pointers for the UTP. In J. S. Fitzgerald, A. E. Haxthausen & H. Yenigun (Eds.), Theoretical Aspects of Computing - ICTAC 2008: 5th International Colloquium, Istanbul, Turkey, September 1-3, 2008. Proceedings (pp. 141-155). Springer. https://doi.org/10.1007/978-3-540-85762-4_10

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

G. Aydal, E., Freeman Paige, R., Utting, M. & Woodcock, J. (2009). Putting Formal Specifications under the Magnifying Glass: Model-based Testing for Validation. In 2009 International Conference on Software Testing Verification and Validation (Vol. 1, pp. 131-140). IEEE. https://doi.org/10.1109/ICST.2009.20

G. Aydal, E., Freeman Paige, R. & Woodcock, J. (2008). Observations for Assertion-based Scenarios in the context of ModelValidation. In T. Margaria, J. Padberg, G. Taentzer, J. Cabot, M. Gogolla & P. Van Gorp (Eds.), Electronic Communications of the EASST: Proceedings of the8th International Workshop onOCL Concepts and Tools (OCL 2008)at MoDELS 2008 https://journal.ub.tu-berlin.de/eceasst/article/view/181/178

G. Aydal, E., Utting, M. & Woodcock, J. (2008). A Comparison of State-Based Modelling Tools for Model Validation. In R. F. Paige & B. Meyer (Eds.), Objects, Components, Models and Patterns: 46th International Conference, TOOLS EUROPE 2008, Zurich, Switzerland, June 30 - July 4, 2008. Proceedings (Vol. 1, pp. 278-296). Springer. https://doi.org/10.1007/978-3-540-69824-1

G. Aydal, E., Freeman Paige, R. & Woodcock, J. (2007). Evaluation of OCL for Large-Scale Modelling: A Different View of the Mondex Purse. In H. Giese (Ed.), Models in Software Engineering: Workshops and Symposia at MoDELS 2007, Nashville, TN, USA, September 30 - October 5, 2007, Reports and Revised Selected Papers (pp. 194-205). Springer. https://doi.org/10.1007/978-3-540-69073-3_21

G. Aydal, E., Freeman Paige, R. & Woodcock, J. (2008). Observations for Assertion-based Scenarios in the context of Model Validation and Extension to Test Case Generation. In 2008 IEEE International Conference on Software Testing Verification and Validation Workshop (pp. 11-20). IEEE. https://doi.org/10.1109/ICSTW.2008.29

G. Aydal, E., Woodcock, J. & Cavalcanti, A. L. C. (2007). Goal-Oriented Automatic Test Case Generators for MC/DC Compliancy. In J. Filipe, M. Helfert & B. Shishkov (Eds.), Proceedings of the Second International Conference on Software and Data Technologies - Volume 1: ICSOFT (Vol. 1: ICSOFT, pp. 290-295.). SCITEPRESS Digital Library. https://doi.org/10.5220/0001324002900295

Gardiner , P. H. B., Lupton, P. J. & Woodcock, J. (1990). A Simpler Semantics for Z. In J. E. Nicholls (Ed.), Proceedings of the Fifth Annual Z User Meeting on Z User Workshop (pp. 3-11). Springer. https://doi.org/10.1007/978-1-4471-3540-1_1

Freitas, L., Woodcock, J. & Fu, Z. (2008). POSIX file store in Z/Eves: An experiment in the verified software repository. Science of Computer Programming, 74(4), 238-257. https://doi.org/10.1016/j.scico.2008.08.001

Freitas, L., Woodcock, J. & Zhang, Y. (2008). Verifying the CICS File Control API with Z/Eves: An experiment in the verified software repository. Science of Computer Programming, 74(4), 197-218. https://doi.org/10.1016/j.scico.2008.09.012

Freitas, L. & Woodcock, J. (2008). FDR Explorer. Formal Aspects of Computing, 21, 133–154. https://doi.org/10.1007/s00165-008-0074-7

Freitas, L. & Woodcock, J. (2007). Mechanising Mondex with Z/Eves. Formal Aspects of Computing, 20(1), 117–139. https://doi.org/10.1007/s00165-007-0059-y

Displaying results 51 to 100 out of 161

Revised 13.11.2025

James Woodcock