Aarhus Universitets segl

Publications

Sortér efter: Dato | Forfatter | Titel

Freitas, L., Mokos, K. & Woodcock, J. (2007). Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository. I 2007 IEEE International Conference on Engineering of Complex Computer Systems (Bind 1, s. 290-298). IEEE. https://doi.org/10.1109/ICECCS.2007.45
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
Schneider, S., Cavalcanti, A. L. C., Treharne, H. & Woodcock, J. (2006). A Layered Behavioural Model of Platelets. I 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
Nuka, G. & Woodcock, J. (2006). Mechanising a Unifying Theory. I S. Dunne & B. Stoddart (red.), Unifying Theories of Programming: First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006, Revised Selected Papers (s. 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. I S. Dunne & B. Stoddart (red.), Unifying Theories of Programming: First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006, Revised Selected Papers (s. 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. I Z. Liu & J. He (red.), Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006. Proceedings (s. 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. I S. Dunne & B. Stoddart (red.), Unifying Theories of Programming: First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006, Revised Selected Papers (s. 123-140). Springer. https://doi.org/10.1007/11768173_8
Woodcock, J. (2006). Verified Software Grand Challenge. I J. Misra, T. Nipkow & E. Sekerinski (red.), FM 2006: Formal Methods: 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006. Proceedings (s. 617-617). Springer. https://doi.org/10.1007/11813040_45
Woodcock, J. & Freitas, L. (2006). Z/Eves and the Mondex Electronic Purse. I K. Barkaoui, A. Cavalcanti & A. Cerone (red.), Theoretical Aspects of Computing - ICTAC 2006: Third International Colloquium, Tunis, Tunisia, November 20-24, 2006. Proceedings (s. 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. I S. Prehn & H. Toetenel (red.), VDM '91 Formal Software Development Methods: 4th International Symposium of VDM Europe Noordwijkerhout, The Netherlands, October 21–25, 1991 Proceedings (s. 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. I D. Gollmann (red.), Computer Security — ESORICS 94: Third European Symposium on Research in Computer Security Brighton, United Kingdom, November 7–9, 1994 Proceedings (s. 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. I J. Fitzgerald, I. J. Hayes & A. Tarlecki (red.), FM 2005: Formal Methods: International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005. Proceedings (s. 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. I D. Bjørner, C. A. R. Hoare & H. Langmaack (red.), VDM '90 VDM and Z — Formal Methods in Software Development: Third International Symposium of VDM Europe Kiel, FRG, April 17–21, 1990 Proceedings (s. 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. I 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. I R. E. . Bloomfield, L. S. Marshall & R. B. Jones (red.), VDM '88 VDM — The Way Ahead: 2nd VDM-Europe Symposium Dublin, Ireland, September 11–16, 1988 Proceedings (s. 434-458). Springer. https://doi.org/10.1007/3-540-50214-9_27
Meyer, B. & Woodcock, J. (red.) (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. I B. Meyer & J. Woodcock (red.), 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 (Bind 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
Woodcock, J. & Cavalcanti, A. (2004). A Tutorial Introduction to Designs in Unifying Theories of Programming. I E. A. Boiten, J. Derrick & G. Smith (red.), Integrated Formal Methods: 4th International Conference, IFM 2004, Cnaterbury, UK, April 4-7, 2004. Proceedings (s. 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. I 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. I D. Kozen (red.), Mathematics of Program Construction: 7th International Conference, MPC 2004, Stirling, Scotland, UK, July 12-14, 2004. Proceedings (s. 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. I K. Araki, S. Gnesi & D. Mandrioli (red.), FME 2003: Formal Methods: International Symposium of Formal Methods Europe. Pisa, Itlay, September 2003. Proceedings (s. 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
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
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. I L.-H. Eriksson & P. A. Lindsay (red.), FME 2002:Formal Methods—Getting IT Right: International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22–24, 2002 Proceedings (s. 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. I D. Bert, J. P. Bowen, M. C. Henson & K. Robinson (red.), 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 (s. 184-203). Springer. https://doi.org/10.1007/3-540-45648-1_10
Woodcock, J. & Hughes, A. (2002). Unifying Theories of Parallel Programming. I C. George & H. Miao (red.), Formal Methods and Software Engineering: 4th International Conference on Formal Engineering Methods, ICFEM 2002 Shanghai, China, October 21–25, 2002 Proceedings (s. 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. I A. Butterfield, G. Strong & C. Pahl (red.), IW-FM'01: Proceedings of the 5th Irish conference on Formal Methods (s. 93–115). BCS Learning & Development Ltd. https://dl.acm.org/doi/10.5555/2227391.2227398
Bolton, C., Davies, J. & Woodcock, J. (1999). On the Refinement and Simulation of Data Types and Processes. I K. Araki, A. Galloway & K. Taguchi (red.), IFM’99: Proceedings of the 1st International Conference on Integrated Formal Methods, York, 28-29 June 1999 (s. 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