Publications

Sort by: Date | Author | Title

Schneider, S., Cavalcanti, A. L. C., Treharne, H. & Woodcock, J. (2006). A Layered Behavioural Model of Platelets. In 11th IEEE International Conference on Engineering of Complex Computer Systems IEEE. https://doi.org/10.1109/ICECCS.2006.1690359

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

Woodcock, J. (2006). First Steps in the Verified Software Grand Challenge. Computer, 39(10), 57-64. https://doi.org/10.1109/MC.2006.340

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

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

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

Bicarregui, J. C. . Hoare, C. A. R. & Woodcock, J. (2006). The verified software repository: a step towards the verifying compiler. Formal Aspects of Computing, 18(2), 143–151. https://doi.org/10.1007/s00165-005-0079-4

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

Woodcock, J. (2006). Verified Software Grand Challenge. In J. Misra, T. Nipkow & E. Sekerinski (Eds.), FM 2006: Formal Methods: 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006. Proceedings (pp. 617-617). Springer. https://doi.org/10.1007/11813040_45

Woodcock, J. & Freitas, L. (2006). Z/Eves and the Mondex Electronic Purse. In K. Barkaoui, A. Cavalcanti & A. Cerone (Eds.), Theoretical Aspects of Computing - ICTAC 2006: Third International Colloquium, Tunis, Tunisia, November 20-24, 2006. Proceedings (pp. 15-34). Springer. https://doi.org/10.1007/11921240_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

Woodcock, J. (2005). A tutorial on the refinement calculus. In S. Prehn & H. Toetenel (Eds.), VDM '91 Formal Software Development Methods: 4th International Symposium of VDM Europe Noordwijkerhout, The Netherlands, October 21–25, 1991 Proceedings (pp. 79-140). Springer. https://doi.org/10.1007/BFb0019996

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

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

Woodcock, J., Cavalcanti, A. L. C. & Freitas, L. (2005). Operational Semantics for Model Checking Circus. In J. Fitzgerald, I. J. Hayes & A. Tarlecki (Eds.), FM 2005: Formal Methods: International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005. Proceedings (pp. 237-252). Springer. https://doi.org/10.1007/11526841_17

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

Woodcock, J. & Morgan, C. (2005). Refinement of state-based concurrent systems. In D. Bjørner, C. A. R. Hoare & H. Langmaack (Eds.), VDM '90 VDM and Z — Formal Methods in Software Development: Third International Symposium of VDM Europe Kiel, FRG, April 17–21, 1990 Proceedings (pp. 340-351). Springer. https://doi.org/10.1007/3-540-52513-0_18

Atiya, D., King, S. & Woodcock, J. (2005). Simpler Reasoning About System Properties: a Proof-by-Refinement Technique. Electronic Notes in Theoretical Computer Science, 137(2), 5-22. https://doi.org/10.1016/j.entcs.2005.04.022

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

Woodcock, J. (2005). Unifying Program Refinement Calculi. In Proceedings of the 12th International Workshop on Abstract State Machines, ASM 2005, March 8-11, 2005, Paris, France https://www.researchgate.net/publication/221612404_Unifying_Program_Refinement_Calculi

Woodcock, J. (2005). Using VDM with rely and guarantee-conditions: Experiences from a real project. In R. E. . Bloomfield, L. S. Marshall & R. B. Jones (Eds.), VDM '88 VDM — The Way Ahead: 2nd VDM-Europe Symposium Dublin, Ireland, September 11–16, 1988 Proceedings (pp. 434-458). Springer. https://doi.org/10.1007/3-540-50214-9_27

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

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

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

Woodcock, J. & Cavalcanti, A. (2004). A Tutorial Introduction to Designs in Unifying Theories of Programming. In E. A. Boiten, J. Derrick & G. Smith (Eds.), Integrated Formal Methods: 4th International Conference, IFM 2004, Cnaterbury, UK, April 4-7, 2004. Proceedings (pp. 40-66). Springer. https://doi.org/10.1007/978-3-540-24756-2_4

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

Tang, X. & Woodcock, J. (2004). Towards Mobile Processes in Unifying Theories. In Proceedings of the Second International Conference on Software Engineering and Formal Methods, 2004. SEFM 2004. IEEE. https://doi.org/10.1109/SEFM.2004.1347502

Tang, X. & Woodcock, J. (2004). Travelling Processes. In D. Kozen (Ed.), Mathematics of Program Construction: 7th International Conference, MPC 2004, Stirling, Scotland, UK, July 12-14, 2004. Proceedings (pp. 381-399). Springer. https://doi.org/10.1007/978-3-540-27764-4_20

Woodcock, J. (2004). Using Circus for Safety-critical Applications. Electronic Notes in Theoretical Computer Science, 95, 3-22. https://doi.org/10.1016/j.entcs.2004.04.003

Atiya, D.-A., King, S. & Woodcock, J. (2003). A Circus Semantics for Ravenscar Protected Objects. In K. Araki, S. Gnesi & D. Mandrioli (Eds.), FME 2003: Formal Methods: International Symposium of Formal Methods Europe. Pisa, Itlay, September 2003. Proceedings (pp. 617-635). Springer. https://books.google.dk/books?id=nqZqCQAAQBAJ&printsec=frontcover&hl=da#v=onepage&q&f=false

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

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

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

Butterfield, A. & Woodcock, J. (2003). Semantic Domains for Handel-C. Electronic Notes in Theoretical Computer Science, 74, 1-20. https://doi.org/10.1016/S1571-0661(04)80762-X

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

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

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

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

Woodcock, J. & Cavalcanti, A. L. C. (2002). The Semantics of Circus. In D. Bert, J. P. Bowen, M. C. Henson & K. Robinson (Eds.), ZB 2002:Formal Specification and Development in Z and B: 2nd International Conference of B and Z Users Grenoble, France, January 23–25, 2002 Proceedings (pp. 184-203). Springer. https://doi.org/10.1007/3-540-45648-1_10

Woodcock, J. & Hughes, A. (2002). Unifying Theories of Parallel Programming. In C. George & H. Miao (Eds.), Formal Methods and Software Engineering: 4th International Conference on Formal Engineering Methods, ICFEM 2002 Shanghai, China, October 21–25, 2002 Proceedings (pp. 24-37). Springer. https://doi.org/10.1007/3-540-36103-0_5

Woodcock, J. & Cavalcanti, A. L. C. (2001). A Concurrent Language for Refinement. In A. Butterfield, G. Strong & C. Pahl (Eds.), IW-FM'01: Proceedings of the 5th Irish conference on Formal Methods (pp. 93–115). BCS Learning & Development Ltd. https://dl.acm.org/doi/10.5555/2227391.2227398

Wing, J. & Woodcock, J. (2000). Introduction: Special Issues for FM'99, the First World Congress on Formal Methods in the Development of Computing Systems. Formal Methods in System Design, 17, 199–200. https://doi.org/10.1023/A:1026521916117

Wing, J. & Woodcock, J. (2000). The First World Congress on Formal Methods in the Development of Computing Systems. Formal Aspects of Computing, 12, 145-146. https://doi.org/10.1007/PL00011167

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

Bolton, C., Davies, J. & Woodcock, J. (1999). On the Refinement and Simulation of Data Types and Processes. In K. Araki, A. Galloway & K. Taguchi (Eds.), IFM’99: Proceedings of the 1st International Conference on Integrated Formal Methods, York, 28-29 June 1999 (pp. 273-292). Springer. https://doi.org/10.1007/978-1-4471-0851-1

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

Stepney, S., Cooper, D. & Woodcock, J. (1998). More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement. In J. P. Bowen, A. Fett & M. G. Hinchey (Eds.), ZUM ’98: The Z Formal Specification Notation: 11th International Conference of Z Users, Berlin, Germany, September 24-26, 1998. Proceedings (Vol. 1, pp. 284-307). Springer Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_20

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

Displaying results 101 to 150 out of 159

Revised 10.08.2023

James Woodcock