Publications by Software Engineering & Computing Systems

Are you looking for publications by Section of Software Engineering & Computing Systems? On this page you can find all the publications made by the Section of Software Engineering & Computing Systems - Department of Electrical and Computer Engineering, Aarhus University.

Below you can find a list of all the publications, their publishing date, their author(s), and titles. The list can be sorted by date, author, and title:

List of Publications

Sort by: Date | Author | Title

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

Woodcock, J. (1991). Two Refinement Case Studies. 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. 118-140). Springer. https://doi.org/10.1007/BFb0019996

Woodcock, J. (1991). 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. 80-95). Springer. https://doi.org/10.1007/BFb0019996

Woodcock, J. (1991). An Introduction to Refinement in Z: A tutorial on the refinement calculus. In S. Prehn & W. J. Toetenel (Eds.), VDM´91 Formal Software Development Methods (Vol. 2, pp. 96-117). Springer Verlag. https://doi.org/10.1007/BFb0019996

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

Woodcock, J., Gardiner , P. H. B. & Hulance, J. R. (1994). The Formal Specification in Z of Defence Standard 00-56. In J. P. Bowen & J. A. Hall (Eds.), Z User Workshop (pp. 9-28). Springer/BCS. https://doi.org/10.1007/978-1-4471-3452-7

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

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

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

Kamari, A., Li, B. & Schultz, C. P. L. (2021). Navigating the vast landscape of spatially valid renovation scenarios. In V. Semenov & R. J. Scherer (Eds.), ECPPM 2021 - eWork and eBusiness in Architecture, Engineering and Construction: Proceedings of the 13th European Conference on Product & Process Modelling (ECPPM 2021), 15-17 September 2021, Moscow, Russia (pp. 163-170). CRC Press/Balkema. https://doi.org/10.1201/9781003191476-22

Badicu, A., Iordache, G., Suciu, G., Macedo, H. D., Sassanelli, C., Terzi, S. & Larsen, P. G. (2021). Deploying the Smart Energy Tool for Investment Simulation inside the HUBCAP Sandbox. In A. G. Bruzzone, J. S. Janosy, L. Nicoletti & G. Zacharewicz (Eds.), 9th International Workshop on Simulation for Energy, Sustainable Development and Environment, SESDE 2021 (pp. 18-26) https://doi.org/10.46354/i3m.2021.sesde.003

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

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

Johansen, K. W., Nielsen, R. O., Teizer, J. & Schultz, C. P. L. (2021). An AI-based approach for automated work progress estimation from construction activities using abductive reasoning. In V. Semenov & R. J. Scherer (Eds.), ECPPM 2021 – eWork and eBusiness in Architecture, Engineering and Construction: Proceedings of the 13th European Conference on Product & Process Modelling (ECPPM 2021), 15-17 September 2021, Moscow, Russia (pp. 237-244). CRC Press. https://doi.org/10.1201/9781003191476-33

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

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

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

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

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

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

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

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

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

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

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. University of York Technical Report Vol. YCS-2002-347 https://www-users.cs.york.ac.uk/~susan/bib/ss/z/347.pdf

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Displaying results 301 to 350 out of 1028

Back to the main page

Revised 13.11.2025

AU Engineering