|
Jim Woodcock
|
|
||||||||||||
|
|
|
||||||||||||
|
|
Formal Methods survey paper now published: Woodcock, Larsen, Bicarregui, & Fitzgerald. Formal Methods: Practice and Experience. ACM Comput. Surv. 41(4): (2009).
Brief biography
Jim Woodcock holds the Anniversary Chair in Software Engineering at the
University of York. Previously, he was Professor of Software Engineering at the
University of Oxford, where he founded the Centre of Excellence in Software
Engineering and directed its academic Programme, which has attracted hundreds
of part-time students from all over the world.
His current research interests include industrial-scale software
engineering, unifying theories of programming, railway signalling, hybrid
control systems, and model checking state-rich concurrent systems.
His research team won the Queen's Award for Technological
Achievement in 1992 for its work with IBM. He was the academic consultant for
the first product certified to ITSEC Level E6 (in 1998), and served for over
ten years as an advisor on secure systems to the British and US governments. In
2002, he won the Rudolf Christian Carl Diesel Prize from the Society for Design
and Process Science.
He is the moderator for UKCRC's Grand Challenge 6 and a co-director
of the United Nations Summer Schools on Theoretical Computer Science. He is
Joint Editor-in-Chief of Formal Aspects of Computing Journal; he has served on
over sixty international conference programme committees, and has chaired
fifteen of them. He has given invited papers and keynote speeches at over
thirty conferences, and is the author of nearly 200 scientific papers and
books. He is currently a Visiting Professor at Trinity College Dublin, Shanghai
Jiao Tong University, and the Federal University of Pernambuco, and a Visiting
Fellow at the University of Oxford, and has twice served as the Formal Methods
Europe Lecturer on lecture tours in South America, and twice for the British
Council in Central Europe and North Africa. He is a Chartered Fellow of the
BCS.
He has acted as a consulting software engineer for many
organisations, including British Energy, DEC, General Dynamics, IBM, LDRA,
Logica, QinetiQ, and the UK Health & Safety Executive.
Publications
Publications ::= Books | Monographs |
Edited volumes | Book
chapters | Journal papers | Refereed conferences | Electronic publications | Selected reports
Books
1.
J. Woodcock, M. Loomes, Software Engineering Mathematics,
Pitman and Addison-Wesley, 1988, 291pp. BibTeX
2.
J. Woodcock, J. Davies, Using Z—Specification, Refinement, and
Proof, Prentice Hall International Series in Computer Science, 1996,
392pp. BibTeX
Monographs
1.
S. King, I. Sørensen, J. Woodcock, Z: Grammar and Concrete and
Abstract Syntaxes, PRG Technical Monograph PRG-66, Oxford University
Computing Laboratory, Programming Research Group, 1988, 48pp. BibTeX
2.
S. Stepney, D. Cooper, J. Woodcock, An Electronic Purse:
Specification, Refinement, and Proof, Technical Monograph PRG-126, Oxford
University Computing Laboratory, 2000, 232pp. BibTeX
3.
D. Cooper, S. Stepney, J. Woodcock, Derivation of Refinement
Proof Rules for Z: forwards and backwards rules incorporating input/output
refinement, Technical Monograph PRG-127, Oxford University Computing
Laboratory, 2000, 201pp. BibTeX
Edited volumes
1.
C. Morgan, J. Woodcock (eds), 3rd Refinement Workshop,
Workshops in Computing Series, Springer, 1990, 197pp. BibTeX
2.
R. Bird, C. Morgan, J. Woodcock (eds), Mathematics of Program
Construction, Second International Conference, Oxford, 29 Jun–3 Jul 1992,
Proceedings, LNCS 669, Springer, 1993, 378pp. BibTeX
3.
J. Woodcock, P. Larsen (eds), FME’93: Industrial-Strength Formal
Methods, First International Symposium of Formal Methods Europe, Odense, Denmark,
19–23 Apr 1993, Proceedings, LNCS 670, Springer, 1993, 670pp. BibTeX
4.
M.-C. Gaudel, J. Woodcock (eds), FMEÂ’96: Industrial Benefit and
Advances in Formal Methods, Third International Symposium of Formal Methods
Europe, Oxford, LNCS 1051, Springer, 1996, 704pp. BibTeX
5.
J. Wing, J. Woodcock, J. Davies (eds), FM’99: Formal Methods,
World Congress on Formal Methods in the Development of Computing Systems,
Toulouse, France, 20–24 Sep 1999, Volume I, LNCS 1708, Springer, 1999. BibTeX
6.
J. Wing, J. Woodcock, J. Davies (eds), FM’99: Formal Methods,
World Congress on Formal Methods in the Development of Computing Systems,
Toulouse, France, 20–24 Sep 1999, Proceedings, Volume II, LNCS 1709, Springer,
1999. BibTeX
7.
J. Davies, A. W. Roscoe, J. Woodcock (eds), Millennial
Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft
Symposium in Honour of Sir Tony Hoare, Palgrave, 2000, 416pp. BibTeX
8.
J. S. Dong, J. Woodcock (eds), Formal Methods and Software
Engineering, 5th International Conference on Formal Engineering Methods,
ICFEM 2003, Singapore, Nov 5–7, 2003, Proceedings, LNCS 2885, Springer,
2003. BibTeX
9.
A. Cavalcanti, A. Sampaio, J. Woodcock (eds), Refinement
Techniques in Software Engineering: First Pernambuco Summer School on Software
Engineering, PSSE 2004, Recife, Brazil, 23 Nov–5 Dec 2004, Revised
Lectures, LNCS 3167, 2006, 394pp. BibTeX
10.
C. Jones, Z. Liu, J. Woodcock (eds), Essays in Honour of Dines
Bjørner and Zhou Chaochen on the Occasion of their 70th Birthdays, Papers
presented at a Festschrift Symposium held in Macao on 24–25 Sep 2007, LNCS
4700, Springer, 2007, 550pp. BibTeX
11.
C. George, Z. Liu, J. Woodcock (eds), Domain Modelling and the
Duration Calculus International Training School, Shanghai, China, 17th–21st
Sep 2007, Advanced Lectures, LNCS 4710, Springer, 2007, 251pp. BibTeX
12.
C. Jones, Z. Liu, J. Woodcock (eds), Proceedings of the
International Colloquium on Theoretical Aspects of Computing, Macao 26–28
Sep 2007, LNCS 4711, Springer, 2007, 481pp.
13.
B. Meyer, J. Woodcock (eds), VSTTE: Verified Software—Theories,
Tools, and Experiments, Proceedings IFIP Working Conference, ETH Zurich,
10–13 Oct 2005, LNCS 4171, Springer, 2007. BibTeX
Book chapters
1.
J. Woodcock, Notes on the Formal Specification of a Programming
Support Environment, in D. Ince (ed.) Software Engineering: the Decade of
Change, pp.100–114, Peter Peregrinus, London, 1986. BibTeX
2.
J. Woodcock, Mathematics as a Management Tool: Proof Rules for
Promotion, in B. A. Kitchenham (ed.), Software Engineering for Large
Software Systems, Elsevier, 1989. BibTeX
3.
J. Woodcock, Simple Transaction Processing and CSP, in P. N.
Scharbach (ed.), Formal Methods: Theory and Practice, Blackwells, 1989,
pp.138-161. BibTeX
4.
J. Woodcock, Using Rely and Guarantee Conditions: Experiences from
a Real Project, in J. A. McDermid (ed.), The Theory and Practice of
Refinement: Approaches to the Formal Development of Large Systems,
Butterworths, 1989. pp.191-217. BibTeX
5.
J. Woodcock, The Applicability of Formal Methods, in D. Craigen
(ed.) and K. Summerskill (assistant ed.), Formal Methods for Trustworthy
Computer Systems (FM89), Workshops in Computing Series, Springer, 1990.
pp.63-67. BibTeX
6.
J. Woodcock, Z, in Dan Craigen (ed.) and Karen Summerskill
(assistant ed.), Formal Methods for Trustworthy Computer Systems (FM89),
Workshops in Computing Series. Springer, 1990. BibTeX
7.
J. Woodcock, C. C. Morgan, What is a Specification? in Dan Craigen
(ed.) and Karen Summerskill (assistant ed.), Formal Methods for Trustworthy
Computer Systems (FM89), Workshops in Computing Series, Springer, 1990.
pp.33-37. BibTeX
8.
S. Brien, J. Woodcock, Semantic Metalanguage, Semantic Universe, Expression,
Predicate, Declaration, Schema, A Deductive System for Z, (7 chapters) in Z
Base Standard Version 1.0, Technical Monograph PRG-107. Oxford University
Programming Research Group, Nov 1992. BibTeX
9.
J. Woodcock, J. Davies, C. Bolton, Abstract Data Types and
Processes, in J. Davies, A. W. Roscoe, and J. Woodcock, (eds), Proceedings
of the Symposium in Honour of C. A. R. Hoare, Palgrave, 2000.
pp.391-405. BibTeX
10.
J. Woodcock, Unifying Theories of Parallel Programming, in Logic
and Algebra for Engineering Software, IOS Press, 2003. BibTeX
11.
A. Cavalcanti, A. Sampaio and J. Woodcock, Refinement: An Overview,
in Refinement Techniques in Software Engineering, LNCS 3167, 2006.
BibTeX
12.
A. Cavalcanti, J. Woodcock, A Tutorial Introduction to CSP in
Unifying Theories of Programming, in Refinement Techniques in Software
Engineering LNCS 3167, pp.220–268, Springer, 2006. BibTeX
13.
L. Freitas, J. Woodcock. Proving Theorems about JML Classes. Essays
in Honour of Dines Bjørner and Zhou Chaochen on the Occasion of their 70th Birthdays,
Papers presented at a Symposium held in Macao on 24th & 25th Sep 2007. LNCS
4700, Springer, 2007. BibTeX
14.
J. Woodcock, Z Logic and its Applications, in D. Bjørner, M. Henson
(eds), Logics of Formal Specification Languages, Springer, 2007. BibTeX
Journal papers
1.
J. Woodcock, Software specification and design for the VLSI era, GEC
Journal of Science & Technology 48(2):86–89 1982. BibTeX
2.
J. Woodcock, The formal specification of a lift system in Milner’s
CCS, Software Engineering Journal May 1987. BibTeX
3.
J. Woodcock, Towards the formal specification of a programming support
environment, Software Engineering Journal Jul 1987. BibTeX
4.
J. Woodcock, Transaction processing primitives and CSP, IBM
Journal of Research & Development 31(5):535–545 1987. BibTeX
5.
J. Woodcock, Structuring specifications in Z, Software
Engineering Journal Jul 1988. BibTeX
6.
J. Woodcock, Formal techniques and operational specifications, Software
Engineering Notes 14 1989. BibTeX
7.
J. Woodcock, The rudiments of algorithm refinement, Computer
Journal 35(5):441–450 1992. BibTeX
8.
J. Sinclair, J. Woodcock, Event refinement in state-based
concurrent systems, Formal Aspects of Computing Journal 7(3):266–288
1995. BibTeX
9.
J. Woodcock, P. Larsen, Introduction to special section (Guest
Editorial), IEEE Transactions on Software Engineering 21(2):61–62
1995. BibTeX
10.
E. M. Clark, J. Wing, J. Woodcock, et al, Formal methods: state of
the art and future directions, ACM Computing Surveys 28(4):626–643
1996. BibTeX
11.
A. P. Martin, P. H. B. Gardiner, J. Woodcock, A tactic
calculus—abridged version, Formal Aspects of Computing Journal 8(4):479–489
1996. BibTeX
12.
A. W. Roscoe, J. Woodcock, L. Wulf, Non-interference through
determinism, Journal of Computer Security 4(1):27–54 1996. BibTeX
13.
A. Cavalcanti, A. Sampaio, J. Woodcock, Procedures and recursion in
the refinement calculus, Journal of the Brazilian Computer Society 5(1):1–15
1998. BibTeX
14.
A. Cavalcanti, J. Woodcock, A weakest precondition semantics for Z,
Computer Journal 41(1):1–15 1998. BibTeX
15.
A. Cavalcanti, J. Woodcock, ZRC—a refinement calculus for Z, Formal
Aspects of Computing Journal 10(3):267–289 1998. BibTeX
16.
A. Cavalcanti, A. Sampaio, J. Woodcock, An inconsistency in
procedures, parameters, and substitution in the refinement calculus, Science
of Computer Programming 33(1):87–96 1999. BibTeX
17.
J. Wing, J. Woodcock, Introduction: Special Issues for FM’99: the
First World Congress on Formal Methods in the Development of Computing Systems,
Guest eds, Formal Aspects of Computing Journal 12(3):145–146 2000.
BibTeX
18.
J. Wing, J. Woodcock, 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(3): 199–200 (2000). BibTeX
19.
J. Wing, J. Woodcock, Introduction: Special Issues for FM’99: the
First World Congress on Formal Methods in the Development of Computing Systems,
Guest eds, IEEE Transactions on Software Engineering 26(8)673–674 Aug
2000. BibTeX
20.
A. Cavalcanti, A. Sampaio, J. Woodcock, A refinement strategy for Circus,
Formal Aspects of Computing Journal 15(2–3):146–181, 2003. BibTeX
21.
A. Cavalcanti, J. Woodcock Predicate transformers in the semantics
of Circus, IEE Proceedings Software 150(1):85–94 2003. BibTeX
22.
M. Oliveira, A. Cavalcanti, J. Woodcock, ArcAngel: a tactic
language for refinement, Formal Aspects of Computing Journal 15(1):28–47
2003. BibTeX
23.
A. Butterfield, J. Woodcock, prialt in Handel-C: an operational
semantics, International Journal on Software Tools for Technology Transfer 7(3):248–267
2005. BibTeX
24.
A. Cavalcanti, A. Sampaio, J. Woodcock, Unifying classes and
processes, Software and System Modeling 4(3):277–296 2005. BibTeX
25.
M. Oliveira, A. Cavalcanti, J. Woodcock, Formal development of
industrial-scale systems Circus, Innovations in Systems and Software
Engineering 1(2):125–146 2005. BibTeX
26.
Juan Bicarregui, C. A. R. Hoare, J. Woodcock, The verified software
repository: a step towards the verifying compiler, Formal Aspects of
Computing Journal 18(2):143–151 2006. BibTeX
27.
A. Cavalcanti, J. Woodcock, S. Dunne, Angelic nondeterminism in the
unifying theories of programming, Formal Aspects of Computing Journal 18(3):288–307
2006. BibTeX
28.
L. Freitas, J. Woodcock, A. Cavalcanti, State-rich model checking, Innovations
in Systems and Software Engineering 2(1) 2006. BibTeX
29.
C. Jones, P. W. O’Hearn, J. Woodcock, Verified software: a grand
challenge, IEEE Computer 39(4):93–95 2006. BibTeX
30.
J. Woodcock, First steps in the Verified Software Grand Challenge, IEEE
Computer 39(10): 57–64 2006. BibTeX
31.
J. Woodcock, Richard Banach, The Verification Grand Challenge, Computer
Society of India Communications 31(2):33–36 2007. BibTeX
32.
J. Woodcock, Richard Banach, The Verification Grand Challenge, Journal
of Universal Computer Science 13(5):661–668 2007. BibTeX
33.
L. Freitas, J. Woodcock, Mechanising Mondex with Z/EVES, Formal
Aspects of Computing Journal 20(1) 2008. BibTeX
34.
J. Woodcock, S. Stepney, D. Cooper, J. Clark, J. Jacob, The
certification of the Mondex electronic purse to ITSEC Level E6, Formal
Aspects of Computing 20(1) 2008. BibTeX
Refereed conferences
1.
J. Woodcock, Formal specification in industry, in R. Babb and A.
Mili (eds), Workshop Notes, IEEE International Workshop on Models and
Languages for Software Specification and Design, Orlando, Florida, IEEE
Press, 1984. Invited paper. BibTeX
2.
J. Woodcock Formal methods for program specification and
verification, in M. Hennell (ed.), Workshop Notes, 3rd IEEE International
Workshop on Software Specification and Design, London, IEEE Press,
1985. BibTeX
3.
J. Woodcock, Formal specification of the lift problem, in M.
Harandi (ed.), Workshop Notes, 4th IEEE International Workshop on Software Specification
and Design, Monterey, California, IEEE Press, 1987. BibTeX
4.
J. Woodcock, B. Dickinson, Using VDM with rely and
guarantee-conditions — Experiences from a real project, in R. Bloomfield, L.
Marshall, R. Jones (eds), VDM’88: VDM—The Way Ahead. Proceedings of the 2nd
VDM-Europe Symposium 1988, LNCS 328:434-458. Springer, 1988. BibTeX
5.
J. Woodcock, Calculating properties of Z specifications, Proceedings
of the 5th IEEE International Workshop on Software Specification and Design,
Pittsburgh, 1989. BibTeX
6.
P. H. B. Gardiner, P. J. Lupton, J. Woodcock, A simpler semantics
for Z, J. Nicholls (ed.), Z User Workshop, Oxford 1990, Workshops in
Computing series, pp.3–11, Springer, 1990. BibTeX
7.
J. Woodcock, C. Morgan, Refinement of state-based concurrent
systems, D. Bjørner, C. A. R. Hoare, and H. Langmaack (eds), VDM’90: VDM and
Z—Formal Methods in Software Development. Third International Symposium of VDM
Europe, LNCS 428:340-351, Springer, 1990. BibTeX
8.
J. Woodcock, An introduction to refinement in Z, in S. Prehn and W.
J. Toetenel (eds), VDM’91: Formal Software Development Methods. 4th
International Symposium of VDM Europe, LNCS 552:96–117. Springer,
1991. BibTeX
9.
J. Woodcock, The refinement calculus, in S. Prehn and W. J.
Toetenel (eds), VDM’91: Formal Software Development Methods. 4th
International Symposium of VDM Europe, LNCS 552:80–95, Springer,
1991. BibTeX
10.
J. Woodcock, Two refinement case studies, in S. Prehn and W. J.
Toetenel (eds), VDM’91: Formal Software Development Methods. 4th
International Symposium of VDM Europe, LNCS 552:118– 140, Springer,
1991. BibTeX
11.
J. Woodcock, S. Brien, W: a logic for Z, Z User Workshop,
York 1991, Workshop in Computing Series, pp.77–998, Springer, 1991. BibTeX
12.
J. Woodcock, Implementing promoted operations in Z, in C. Jones, R.
Shaw, T. Denvir (eds), 5th Refinement Workshop, Workshops in Computing
Series, pp.367–378, Springer, 1992. Keynote speech. BibTeX
13.
A. W. Roscoe, J. Woodcock, L. Wulf, Non-interference through
determinism, in D. Gollman (ed.), Computer Security—ESORICS’94. Third European
Symposium on Research in Computer Security, Brighton, LNCS 875:33–54,
Springer, 1994. BibTeX
14.
J. Woodcock, P. H. B. Gardiner, J. Hulance, The formal
specification in Z of Defence Standard 00–56, in J. P. Bowen and J. A. Hall
(eds), Z User Workshop, Cambridge 1994. Workshop in Computing series,
pp.9–28, Springer, 1994. Keynote speech. BibTeX
15.
A. Simpson, J. Woodcock, J. Davies, The mechanical verification of
solid-state interlocking geographic data, in J. Grundy, M. Schwenke, T. Vickers
(eds), Formal Methods Pacific ’97, pp.223– 243, Springer, 1997. BibTeX
16.
A. Simpson, J. Davies, J. Woodcock, Security management via Z and
CSP, in J. Grundy, M. Schwenke, T. Vickers (eds), Formal Methods Pacific
’98/International Refinement Workshop ’98, Springer Series in Discrete
Mathematics and Theoretical Computer Science, pp.334–351, 1998. BibTeX
17.
A. Simpson, J. Woodcock, J. Davies, Safety through security, Proceedings
of the 9th IEEE International Workshop on Software Specification and Design,
Ise-Shima, Japan, IEEE Computer Society Press, pp.18–24, 1998. BibTeX
18.
S. Stepney, D. Cooper, J. Woodcock, More powerful Z data
refinement: pushing the state of the art in industrial refinement, in J. P.
Bowen, A. Fett, M. G. Hinchey (eds), 11th International Conference of Z
Users, Berlin. Sep 1998. LNCS 1493:284–307, Springer, 1998. Winner of the
best paper award. BibTeX
19.
J. Woodcock, Industrial-strength refinement, Proceedings of the
Joint Formal Methods Pacific ’98/International Refinement Workshop ’98 and
Conference on Theorem Proving in Higher-Order Logics, Canberra, Australia,
Sep 1998, Springer Series in Discrete Mathematics and Theoretical Computer
Science, pp.33–44, 1998. Keynote speech. BibTeX
20.
C. Bolton, J. Davies, J. Woodcock, On the refinement and simulation
of abstract data types. in K. Araki, A. Galloway, K. Taguchi (eds), Proceedings
of the Conference on Integrating Formal Methods, IFM99, Springer.
pp.273–292, 1999. BibTeX
21.
C. Crichton, J. Davies, J. Woodcock, When to trust mobile objects:
access control in the Jini Software System, in D. Firesmith, R. Riehle, G.
Pour, B. Meyer (eds), Proceedings of the IEEE Conference on Technology of
Object-Oriented Languages and Systems, IEEE Computer Society Press,
1999. BibTeX
22.
J. Woodcock, Formal refinement: practical industrial experiences, Proceedings
of the 3rd Irish Formal Methods Workshop, IFMW’99, National University of
Ireland, Galway, BCS Electronic Workshops in Computing, 1999. Keynote
speech. BibTeX
23.
J. Woodcock, A. McEwan,S Specifying a Handel-C program in the
Unifying Theory, Proceedings of the Workshop on Parallel Programming,
Las Vegas, Nov 1999. BibTeX
24.
J. Woodcock, A. McEwan, An overview of the verification of a
Handel-C program, Proceedings of the International Conference on Parallel
and Distributed Processing Techniques and Applications, IDPT Press,
2000. BibTeX
25.
J. Woodcock, A. Cavalcanti, A concurrent language for refinement,
in A. Butterfield and C. Pahl (eds), IWFM’01: 5th Irish Workshop in Formal
Methods, Dublin, BCS Electronic Workshops in Computing, 2001. BibTeX
26.
J. Woodcock, A. Cavalcanti, The steam boiler in a unified theory of
Z and CSP, Proceedings of the 8th Asia-Pacific Software Engineering
Conference, Macau, IEEE Computer Society Press, pp.291–298, 2001. BibTeX
27.
A. Butterfield, J. Woodcock, Semantics of prialt in Handel-C, in J.
Pascoe, P. Welch, R. Loader, V. Sunderam (eds), Communicating Process
Architectures 2002, IOS Press, pp.1–16, 2002. BibTeX
28.
A. Butterfield, J. Woodcock, Semantic domains for Handel-C, in 2nd
Irish Conference on the Mathematical Foundations of Computer Science and
Information Technology, Electronic Notes in Theoretical Computer Science
74:1–20 2002. BibTeX
29.
A. Cavalcanti, J. Woodcock, A weakest precondition semantics for Circus,
in J. Pascoe, P. Welch, R. Loader, V. Sunderam (eds), Communicating Process
Architectures 2002, IOS Press, pp.147–166. 2002. BibTeX
30.
A. Cavalcanti, A. Sampaio, J. Woodcock, Refinement of actions in Circus,
Proceedings of REFINE’ 2002, Electronic Notes in Theoretical Computer
Science 70(3) 2002. Keynote speech. BibTeX
31.
A. Sampaio, J. Woodcock, A. Cavalcanti, Refinement in Circus,
L. Eriksson and P. Lindsay (eds), FME 2002: Formal Methods—Getting IT Right,
LNCS 2391:451–470, Springer, 2002. BibTeX
32.
J. Woodcock, A. Cavalcanti, The semantics of Circus—a
concurrent language for refinement, Proceedings of ZB 2002—The 2nd
International Z and B Conference, Grenoble, LNCS. 2272:184–203, Springer,
2002. BibTeX
33.
J. Woodcock, A. Hughes, Unifying theories of parallel programming, 4th
International Conference on Formal Engineering Methods, ICFEM 2002,
Shanghai, China, Oct 21–25, 2002, LNCS 2495:24–37 2002. Keynote
speech. BibTeX
34.
J. Woodcock, A. McEwan, Verifying the properties of a railway
signalling device, Proceedings of the International Conference on Integrated
Design and Process Technology, Pasadena, IDPT Press, Jun 2002. Rudolph
Christian Karl Diesel best paper award. BibTeX
35.
D.-A. Atiya, S. King, J. Woodcock, A Circus semantics for
Ravenscar protected objects, FM 2003: 12th International FME Symposium,
Pisa, LNCS 2805:617–635 2003. BibTeX
36.
A. Butterfield, J. Woodcock, An operational semantics for Handel-C,
FMICS workshop on Formal Methods for Industrial Critical Systems, Electronic
Notes in Theoretical Computer Science 80 2003. BibTeX
37.
A. Cavalcanti, A. Sampaio, J. Woodcock, A unified language of
classes and processes, St.Eve: State-Oriented vs Event-Oriented Thinking in
Requirements Analysis, Formal Specification, and Software Engineering,
Satellite Workshop at FM’03, 2003. BibTeX
38.
A. McEwan, J. Woodcock, A refinement-based approach to calculating
a fault-tolerant railway signal device, IFIP Congress Topical Sessions 621–628
2004. BibTeX
39.
G. Nuka, J. Woodcock, Mechanising the alphabetised relational
calculus, WMF2003: 6th Brazilian Workshop on Formal Methods Campina Grande,
Brazil, Electronic Notes in Theoretical Computer Science 95:209–225
2004. BibTeXXXXXX
40.
M. Oliveira, A. Cavalcanti, J. Woodcock, Refining industrial-scale
systems in Circus, in I. East, J. Martin, P. Welch, D. Duce, and M.
Green (eds), Communicating Process Architectures, Concurrent Systems
Engineering Series 62:281–309, IOS Press, 2004. BibTeX
41.
X. Tang, J. Woodcock, Towards mobile processes in unifying
theories, in J. R. Cuellar and Z. Liu (eds), 2nd IEEE International
Conference on Software Engineering and Formal Methods, IEEE Computer
Society Press, pp.310–319, Sep 2004. BibTeX
42.
X. Tang, J. Woodcock, Travelling processes, Mathematics of
Program Construction, LNCS 3125 381–399 2004. BibTeX
43.
J. Woodcock, Using Circus for safety-critical applications, WMF2003:
6th Brazilian Workshop on Formal Methods, Campina Grande, Brazil, Electronic
Notes in Theoretical Computer Science 95:3–22 2004. Keynote speech. The
Formal Methods Europe Lecture. BibTeX
44.
J. Woodcock, A. Cavalcanti, A tutorial introduction to designs in
Unifying Theories of Programming, in E. A. Boiten, J. Derrick, G. Smith (eds), IFM
2004: Integrated Formal Methods, LNCS 2999:40–66, Springer, 2004. Invited
lectures. BibTeX
45.
D.-A. Atiya, S. King, J. Woodcock, Simpler reasoning about system
properties: a proof-by-refinement technique, in Proceedings of the REFINE
2005 Workshop (REFINE 2005), Electronic Notes in Theoretical Computer
Science 137(2):5–22 2005. BibTeX
46.
A. Cavalcanti, J. Woodcock, Angelic nondeterminism and Unifying
Theories of Programming, in J. Derrick and E. Boiten (eds), REFINE 2005,
Electronic Notes in Theoretical Computer Science 137(2):45–66
2005. BibTeX
47.
J. Woodcock, A. Cavalcanti, L. Freitas, 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,
LNCS 3582:237–252 Springer, 2005. BibTeX
48.
A. Butterfield, J. Woodcock, A “hardware compiler” semantics for
Handel-C, in Proceedings of the 3rd Irish Conference on the Mathematical
Foundations of Computer Science and Information Technology (MFCSIT 2004)
Electronic Notes in Theoretical Computer Science 161:73–90 2006. BibTeX
49.
A. Cavalcanti, W. Harwood, J. Woodcock, Pointers and records in the
Unifying Theories of Programming, in S. Dunne and B. Stoddart (eds), UTP’06:
International Symposium on Unifying Theories of Programming, Walworth
Castle, LNCS 4010:200–216, Springer, 2006. BibTeX
50.
L. Freitas, A. Cavalcanti, J. Woodcock, Taking our own medicine:
Applying the refinement calculus to state-rich refinement model checking, in Z.
Liu and J. He (eds), Formal Methods and Software Engineering, 8th
International Conference on Formal Engineering Methods, ICFEM 2006,
Guiyang, China, LNCS 4260:697–716, Springer, 2006. BibTeX
51.
G. Nuka, J. Woodcock, Mechanising a unifying theory, in S. Dunne
and B. Stoddart (eds), UTP’06: International Symposium on Unifying Theories
of Programming, Walworth Castle, LNCS 4010:217–235, Springer, 2006. BibTeX
52.
M. Oliveira, A. Cavalcanti, J. Woodcock, Unifying theories in
ProofPower-Z, in S. Dunne and B. Stoddart (eds), UTP’06: International
Symposium on Unifying Theories of Programming, Walworth Castle, LNCS
4010:123–140, Springer 2006. BibTeX
53.
S. Schneider, H. Treharne, A. Cavalcanti, J. Woodcock, A layered
behavioural model of platelets, in Proceedings 11th International Conference
on Engineering of Complex Computer Systems, pp.98–106, IEEE Computer
Society Press, 2006. BibTeX
54.
J. Woodcock, First steps in the Verified Software Grand Challenge, 30th
Annual IEEE / NASA Software Engineering Workshop (SEW-30 2006), 203–206,
25–28 Apr 2006, Loyola College Graduate Center, Columbia, IEEE Computer
Society, 2006. BibTeX
55.
J. Woodcock, Verified Software Grand Challenge, in J. Misra, T.
Nipkow, E. Sekerinski (eds), FM 2006: Formal Methods, 14th International
Symposium on Formal Methods, Hamilton, Canada, Aug 21-27, 2006,
Proceedings, LNCS 4085:617–617, Springer, 2006. BibTeX
56.
J. Woodcock, An operational semantics in UTP for a language of
reactive designs (abstract), in S. Dunne and B. Stoddart (eds), UTP’06:
International Symposium on Unifying Theories of Programming, Walworth
Castle, LNCS 4010:84–84, Springer 2006. BibTeX
57.
J. Woodcock, L. Freitas, Z/Eves and the Mondex electronic purse, Theoretical
Aspects of Computing — ICTAC 2006, LNCS 4281:15–34 2006. BibTeX
58.
E. Aydal, R. Paige, J. Woodcock, Evaluation of OCL for large-scale
modelling: a different view of the Mondex smart card application, Ocl4All:
Modelling Systems with OCL, MODELS’07, Nashville, Sep 2007. BibTeX
59.
E. Aydal, J. Woodcock, A. Cavalcanti, Goal-oriented automatic
test-case generators for MC/DC compliancy, ICSOFT’07, Barcelona, Spain,
Jul 2007. BibTeX
60.
A. Butterfield, A. Sherif, J. Woodcock, Slotted Circus. Integrated
Formal Methods: 6th International Conference, IFM 2007, Oxford, 2–5 Jul
2007, Proceedings, LNCS 4591 2007. BibTeX
61.
A. Butterfield, J. Woodcock, Formalising flash memory: first steps,
ICECCS: 12th International Conference on Engineering of Complex Computer
Systems 2006, Auckland, New Zealand, 2007. BibTeX
62.
L. Freitas, Z. Fu, J. Woodcock, POSIX file store in Z/Eves: An
experiment in the Verified Software Repository, ICECCS: 12th International
Conference on Engineering of Complex Computer Systems 2006, Auckland, New
Zealand, 2007. BibTeX
63.
L. Freitas, K. Mokos, J. Woodcock, Verifying the CICS File Control
API with Z/Eves: An experiment in the Verified Software Repository, ICECCS:
12th International Conference on Engineering of Complex Computer Systems 2006,
Auckland, New Zealand, 2007. BibTeX
64.
L. Freitas, J. Woodcock, FDR Explorer, Electronic Notes in
Theoretical Computer Science 187:19–34 2007. BibTeX
65.
M. Oliveira, A. Cavalcanti, J. Woodcock, A denotational semantics
for Circus, in B. Aichernig and J. Derrick (eds), REFINE’2006, Electronic
Notes in Theoretical Computer Science 187:107–123 2007 . BibTeX
66.
M. Oliveira, J. Woodcock, Automatic generation of verified
concurrent hardware, International Conference on Formal Engineering Methods,
ICFEM 2007, LNCS, Springer, 2007. BibTeX
67.
J. Perna, J. Woodcock, A denotational semantics in HOL for Handel-C
hardware compilation, International Conference on Formal Engineering
Methods, ICFEM 2007, LNCS, Springer, 2007. BibTeX
Electronic publications
1.
J. Woodcock, E6: Use of formality, Video tape G3A tape No. 68,
Government Communications Headquarters, Communications-Electronics Security
Group, Unclassified document, Oct 1997. BibTeX
2.
J. Wing, J. Woodcock, J. Davies, World Congress on Formal
Methods FM99: Proceedings, Tutorials, and additional materials, CD,
Springer, Sep 1999. BibTeX
3.
J. Woodcock, S. Stepney, Software Engineering Research at Oxford, The
Oxford Story, Video recorded interviews, 1999. BibTeX
4.
J. Derrick, E. A. Boiten, J. Woodcock, J. von Wright, Preface, Electronic
Notes in Theoretical Computer Science 70(3) 2002. BibTeX
5.
J. Woodcock, Software Engineering Mathematics, Microsoft
Reader eBook (Windows 98+, Tablet PC, Pocket PC 2003), eBookMall, 2007. BibTeX
Selected Reports
1.
D. Pitt, J. Woodcock, The Importance of Time in the
Specification of OSI Protocols, Report NPLDITC-78/86, National Physical
Laboratory, Teddington, Nov 1986. BibTeX
2.
J. Woodcock, Teaching how to use mathematics for large-scale
software development. Bulletin of BCS-FACS, Jul 1988. BibTeX
3.
J. Woodcock, Case Studies in Proof in Z, DTI IED Zip Project
Deliverable, 1992. BibTeX
4.
J. Woodcock, Standards for the use of Z, Formal Systems
(Europe) Ltd, Technical Memorandum SRC/ZS/1 version 1.4, Dec 1992. BibTeX
5.
J. Woodcock, Interim Defence Standard 00–56 Safety Analysis
Elements: revised formal specification, Formal Systems (Europe) Ltd,
Technical Memorandum SRC/RDS-SAE/1 version 1.9, Apr 1993. BibTeX
6.
J. Woodcock, J. Hulance, A Rigorous Development of a Process
Scheduler, Formal Systems (Europe) Ltd, Technical Memorandum CSDL/PS/1, Feb
1994. BibTeX
7.
ISO Panel, Z Notation: version 1.2. Draft British and
International Standard, available as BSI Panel IST/5/- /19/2 (Z Notation),
ISO Panel JTC1/SC22/WG19 (Rapporteur Group for Z), 14 Sep 1995. 210pp. BibTeX
8.
D. Cooper, S. Stepney, J. Woodcock, Derivation of Z Refinement
Proof Rules: Forwards and Backwards Rules Incorporating Input/Output Refinement,
University of York, Department of Computer Science, YCS-2002-347, 2002. BibTeX
9.
J. Woodcock, A. Cavalcanti, Circus: a Concurrent Refinement
Language, Technical Report, University of Kent and Federal University of
Pernambuco, 2002. BibTeX
10.
J. Woodcock, A. Hughes, Unifying Theories of Parallel
Programming, Notes for Marktoberdorf Summer School, Technical University of
Munich, 2002. BibTeX
11.
D.-A. Atiya, S. King, J. Woodcock, Ravenscar Protected Objects:
a Circus Semantics, Research Report YCS 356(2003), University of York, Dept
of Computer Science, 2003. BibTeX
12.
A. Cavalcanti, J. Woodcock, Angelic Nondeterminism and Unifying
Theories of Programming (Extended Version), Computing Laboratory,
University of Kent, 2004. BibTeX
J. Woodcock, M. Loomes, Software Engineering Mathematics,
Pitman and Addison-Wesley, 1988, 291pp.
@book{%
book:WoodcockLoomes88, %
author = {J. Woodcock and M. Loomes}, %
title = {Software Engineering Mathematics}, %
publisher = {Pitman and Addison-Wesley}, %
year = {1988}, %
size = {291pp.}
}%
J. Woodcock, J. Davies, Using Z—Specification, Refinement, and
Proof, Prentice Hall International Series in Computer Science, 1996, 392pp.
@book{%
book:WoodcockDavies96, %
author = {J. Woodcock and J. Davies},
%
title = {Using Z---Specification,
Refinement, and Proof}, %
publisher = {Prentice Hall International}, %
series = {Series in Computer Science},
%
year = {1996}, %
size = {392pp.} %
}%
monograph:KingSorensenWoodcock88
S. King, I. Sørensen, J. Woodcock, Z: Grammar and Concrete and
Abstract Syntaxes, PRG Technical Monograph PRG-66, Oxford University Computing
Laboratory, Programming Research Group, 1988, 48pp.
@booklet{%
monograph:KingSorensenWoodcock88, %
author = {S. King and I. S{\o}rensen
and J. Woodcock}, %
title = {Z: Grammar and
Concrete and Abstract Syntaxes}, %
type = {PRG Technical
Monograph}, %
number = {PRG-66}, %
organization = {Oxford University Computing Laboratory, Programming
Research Group}, %
year = {1988}, %
size = {48pp.} %
}%
monograph:StepneyCooperWoodcock00
S. Stepney, D. Cooper, J. Woodcock, An Electronic Purse:
Specification, Refinement, and Proof, Technical Monograph PRG-126, Oxford
University Computing Laboratory, 2000, 232pp.
@booklet{%
monograph:StepneyCooperWoodcock00, %
author = {S. Stepney and D. Cooper
and J. Woodcock}, %
title = {An Electronic Purse:
Specification, Refinement, and Proof}, %
type = {Technical
Monograph}, %
number = {PRG-126}, %
organization = { Oxford University Computing Laboratory}, %
year = {2000}, %
size = {232pp.} %
}%
monograph:CooperStepneyWoodcock00
D. Cooper, S. Stepney, J. Woodcock, Derivation
of Refinement Proof Rules for Z: forwards and backwards rules incorporating
input/output refinement, Technical Monograph PRG-127, Oxford
University Computing Laboratory, 2000, 201pp.
@booklet{%
monograph:CooperDStepneyWoodcock00, %
author = {D. Cooper and S. Stepney
and J. Woodcock}, %
title = {Derivation of Refinement
Proof Rules for Z: forwards and backwards rules incorporating input/output
refinement}, %
type = {Technical
Monograph}, %
number = {PRG-127}, %
organization = {Oxford University Computing Laboratory}, %
year = {2000}, %
size = {201pp.} %
}%
C. Morgan, J. Woodcock (eds), 3rd Refinement Workshop,
Workshops in Computing Series, Springer, 1990, 197pp.
@proceedings{%
proceedings:MorganWoodcock90, %
editor = {C. Morgan and J.
Woodcock}, %
title = {3rd Refinement
Workshop}, %
series = {Workshops in Computing
Series}, %
publisher = {Springer}, %
year = {1990}, %
size = {197pp.} %
}%
proceedings:BirdMorganWoodcock93
R. Bird, C. Morgan, J. Woodcock (eds), Mathematics of Program
Construction, Second International Conference, Oxford, 29 Jun–3 Jul 1992,
Proceedings, LNCS 669, Springer, 1993, 378pp.
@proceedings{%
proceedings:BirdMorganWoodcock93, %
editor = {R. Bird and C. Morgan
and J. Woodcock}, %
title = {Mathematics of
Program Construction, Second International Conference, Oxford, 29 June--3 July 1992},
%
series = {LNCS}, %
number = {669}, %
publisher = {Springer}, %
year = {1993}, %
size = {378pp.}
}5 %
J. Woodcock, P. Larsen (eds), FME’93: Industrial-Strength Formal
Methods, First International Symposium of Formal Methods Europe, Odense,
Denmark, 19–23 Apr 1993, Proceedings, LNCS 670, Springer, 1993, 670pp.
@proceedings{%
proceedings:WoodcockLarsen93, %
editor = {J. Woodcock and P.
Larsen}, %
title = {FME’93: Industrial-Strength
Formal Methods, First International Symposium of Formal Methods Europe, Odense,
Denmark, 19--23 Apr 1993}, %
series = {LNCS}, %
number = {670}, %
publisher = {Springer}, %
year = {1993}, %
size = {670pp.} %
}%
M.-C. Gaudel, J. Woodcock (eds), FME’96: Industrial Benefit and
Advances in Formal Methods, Third International Symposium of Formal Methods
Europe, Oxford, LNCS 1051, Springer, 1996, 704pp.
@proceedings{%
proceedings:GaudelWoodcock96, %
editor = {Marie-Claude Gaudel
and Jim Woodcock}, %
title = {FME'96: Industrial
Benefit and Advances in Formal Methods, Third International Symposium of Formal
Methods Europe, Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18-22, 1996,
Proceedings}, %
booktitle = {FME}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {1051}, %
year = {1996}, %
isbm = {3-540-60973-3},
%
}%
proceedings:WingWoodcockDavies99a
J.
Wing, J. Woodcock, J. Davies (eds), FM’99: Formal Methods, World Congress on
Formal Methods in the Development of Computing Systems, Toulouse, France, 20–24
Sep 1999, Volume I, LNCS 1708, Springer, 1999.
@proceedings{%
proceedings:WingWoodcockDavies99a, %
editor = {Jeannette M. Wing and
Jim Woodcock and Jim Davies}, %
title = {FM'99 - Formal
Methods, World Congress on Formal Methods in the Development of Computing Systems,
Toulouse, France, September 20-24, 1999, Proceedings, Volume I}, %
booktitle = {World Congress on Formal Methods},
%
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {1708}, %
year = {1999}, %
isbm = {3-540-66587-0},
%
}%
proceedings:WingWoodcockDavies99b
J.
Wing, J. Woodcock, J. Davies (eds), FM’99: Formal Methods, World Congress on
Formal Methods in the Development of Computing Systems, Toulouse, France, 20–24
Sep 1999, Proceedings, Volume II, LNCS 1709, Springer, 1999.
@proceedings{%
proceedings:WingWoodcockDavies99b, %
editor = {Jeannette M. Wing and
Jim Woodcock and Jim Davies}, %
title = {FM'99 - Formal
Methods, World Congress on Formal Methods in the Development of Computing Systems,
Toulouse, France, September 20-24, 1999, Proceedings, Volume II}, %
booktitle = {World Congress on Formal Methods},
%
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {1709}, %
year = {1999}, %
isbm = {3-540-66588-9},
%
}%
proceedings:DaviesRoscoeWoodcock00
J. Davies, A. W. Roscoe, J. Woodcock (eds), Millennial
Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft
Symposium in Honour of Sir Tony Hoare, Palgrave, 2000, 416pp.
@proceedings{%
proceedings:DaviesRoscoeWoodcock00, %
editor = {J. Davies and A. W.
Roscoe and J. Woodcock}, %
title = {Millennial Perspectives
in Computer Science: Proceedings of the 1999 Oxford-Microsoft Symposium in
Honour of Sir Tony Hoare}, %
publisher = {Palgrave}, %
year = {2000}, %
size = {416pp.} %
}%
J. S. Dong, J. Woodcock (eds), Formal Methods and Software
Engineering, 5th International Conference on Formal Engineering Methods, ICFEM 2003,
Singapore, Nov 5–7, 2003, Proceedings, LNCS 2885, Springer, 2003.
@proceedings{%
proceedings:DongWoodcock03, %
editor = {Jin Song Dong and Jim
Woodcock}, %
title = {Formal Methods
and Software Engineering, 5th International Conference on Formal Engineering Methods,
ICFEM 2003, Singapore, November 5-7, 2003, Proceedings}, %
booktitle = {ICFEM}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {2885}, %
year = {2003}, %
isbm = {3-540-20461-X},
%
}%
proceedings:CavalcantiSampaioWoodcock04
A. Cavalcanti, A. Sampaio, J. Woodcock (eds), Refinement
Techniques in Software Engineering: First Pernambuco Summer School on Software
Engineering, PSSE 2004, Recife, Brazil, 23 Nov–5 Dec 2004, Revised Lectures, LNCS 3167,
2006, 394pp.
@proceedings{%
proceedings:CavalcantiSampaioWoodcock06, %
editor = {A. Cavalcanti, A.
Sampaio, J. Woodcock}, %
title = {Refinement Techniques
in Software Engineering: First Pernambuco Summer School on Software Engineering,
PSSE 2004, Recife, Brazil, 23 Nov--5 Dec 2004, Revised Lectures}, %
series = {LNCS}, %
number = {3167}, %
year = {2006}, %
size = {394pp.} %
}%
proceedings:JonesLiuWoodcock07a
C. Jones, Z. Liu, J. Woodcock (eds), Essays
in Honour of Dines Bjørner and Zhou Chaochen on the Occasion of their 70th
Birthdays, Papers presented at a Festschrift Symposium held in Macao on
24–25 Sep 2007, LNCS 4700, Springer, 2007, 550pp.
@proceedings{%
proceedings:JonesLiuWoodcock07a, %
editor = {Cliff B. Jones and Zhiming
Liu and Jim Woodcock}, %
title = {Formal Methods
and Hybrid Real-Time Systems, Essays in Honour of Dines Bj{\o}rner and Chaochen
Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held
in Macao, China, September 24-25, 2007}, %
booktitle = {Formal Methods and Hybrid Real-Time
Systems}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {4700}, %
year = {2007}, %
isbm = {978-3-540-75220-2},
%
}%
proceedings:GeorgeLiuWoodcock07
C. George, Z. Liu, J. Woodcock (eds), Domain
Modelling and the Duration Calculus, International Training School,
Shanghai, China, 17th–21st Sep 2007, Advanced Lectures, LNCS 4710, Springer,
2007, 251pp.
@proceedings{%
proceedings:GeorgeLiuWoodcock07, %
editor = {Chris George and Zhiming
Liu and Jim Woodcock}, %
title = {Domain Modeling
and the Duration Calculus, International Training School, Shanghai, China, September
17-21 2007, Advanced Lectures}, %
booktitle = {Domain Modeling and the Duration Calculus},
%
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {4710}, %
year = {2007}, %
isbm = {978-3-540-74963-9},
%
}%
proceedings:JonesLiuWoodcock07b
C. Jones, Z. Liu, J. Woodcock (eds), Proceedings
of the International Colloquium on Theoretical Aspects of Computing, Macao
26–28 Sep 2007, LNCS 4711, Springer, 2007, 481pp.
@proceedings{%
proceedings:JonesLiuWoodcock07b, %
editor = {Cliff B. Jones and Zhiming
Liu and Jim Woodcock}, %
title = {Theoretical Aspects
of Computing - ICTAC 2007, 4th International Colloquium, Macau, China, September
26-28, 2007, Proceedings}, %
booktitle = {ICTAC}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {4711}, %
year = {2007}, %
isbm = {978-3-540-75290-5},
%
}%
B. Meyer, J. Woodcock (eds), VSTTE: Verified Software—Theories,
Tools, and Experiments, Proceedings IFIP Working Conference, ETH Zurich,
10–13 Oct 2005, LNCS 4171, Springer, 2007.
@proceedings{%
proceedings:MeyerWoodcock07, %
editor = {B. Meyer and J. Woodcock},
%
title = {VSTTE: Verified
Software---Theories, Tools, and Experiments, Proceedings IFIP Working Conference,
ETH Zurich, 10--13 Oct 2005}, %
series = {LNCS}, %
volume = {4171}, %
publisher = {Springer}, %
year = {2007} %
}%
J. Woodcock, Notes on the Formal Specification of a Programming
Support Environment, in D. Ince (ed.) Software Engineering: the Decade of
Change, pp.100–114, Peter Peregrinus, London, 1986.
@incollection{%
book:Woodcock86, %
author = {J. Woodcock}, %
title = {Notes on the Formal
Specification of a Programming Support Environment}, %
editor = {D. Ince}, %
booktitle = {Software Engineering: the Decade of
Change}, %
pages = {100--114}, %
publisher = {Peter Peregrinus}, %
year = {1986} %
}%
J. Woodcock, Mathematics as a Management Tool: Proof Rules for
Promotion, in B. A. Kitchenham (ed.), Software Engineering for Large Software
Systems, Elsevier, 1989.
@incollection{%
chapter:Woodcock89a, %
author = {J. Woodcock}, %
title = {Mathematics as
a Management Tool: Proof Rules for Promotion}, %
editor = {B. A. Kitchenham}, %
booktitle = {Software Engineering for Large Software
Systems}, %
publisher = {Elsevier}, %
pages = {0--0}, %
year = {1989} %
}%
J. Woodcock, Simple Transaction Processing and CSP, in P. N.
Scharbach (ed.), Formal Methods: Theory and Practice, Blackwells, 1989,
pp.138-161.
@incollection{%
chapter:Woodcock89b, %
author = {J. Woodcock}, %
title = {Simple Transaction
Processing and CSP}, %
editor = {P. N. Scharbach}, %
booktitle = {Formal Methods: Theory and Practice},
%
publisher = {Blackwells}, %
year = {1989}, %
pages = {138--161} %
}%
J. Woodcock, Using Rely and Guarantee Conditions: Experiences from
a Real Project, in J. A. McDermid (ed.), The Theory and Practice of Refinement:
Approaches to the Formal Development of Large Systems,
Butterworths, 1989. pp.191-217.
@inproceedings{%
chapter:WoodcockDickinson88, %
author = {Jim Woodcock and B.
Dickinson}, %
title = {Using VDM with
Rely and Guarantee-Conditions - Experiences from a Real Project}, %
booktitle = {VDM Europe}, %
year = {1988}, %
pages = {434-458}, %
crossref = {proceedings:BloomfieldMarshallJones88},
%
}%
proceedings:BloomfieldMarshallJones88
@proceedings{%
proceedings:BloomfieldMarshallJones88, %
editor = {Robin E. Bloomfield
and Lynn S. Marshall and Roger B. Jones}, %
title = {VDM '88, VDM -
The Way Ahead, 2nd VDM-Europe Symposium, Dublin, Ireland, September 11-16, 1988,
Proceedings}, %
booktitle = {VDM Europe}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {328}, %
year = {1988}, %
isbm = {3-540-50214-9},
%
}%
J. Woodcock, The Applicability of Formal Methods, in D. Craigen
(ed.) and K. Summerskill (assistant ed.), Formal Methods for Trustworthy Computer
Systems (FM89), Workshops in Computing Series, Springer, 1990. pp.63-67.
@incollection{%
chapter:Woodcock90a, %
author = {J. Woodcock}, %
title = {The Applicability
of Formal Methods}, %
editor = {D. Craigen and K. Summerskill},
%
booktitle = {Formal Methods for Trustworthy Computer
Systems (FM89)}, %
series = {Workshops in Computing
Series}, %
publisher = {Springer}, %
year = {1990}, %
pages = {63--67} %
}%
J. Woodcock, Z, in Dan Craigen (ed.) and Karen Summerskill
(assistant ed.), Formal Methods for Trustworthy Computer Systems (FM89),
Workshops in Computing Series. Springer, 1990.
@incollection{%
chapter:Woodcock90b, %
author = {J. Woodcock}, %
title = {Z}, %
editor = {Dan Craigen and Karen
Summerskill}, %
booktitle = {Formal Methods for Trustworthy Computer
Systems (FM89)}, %
series = {Workshops in Computing
Series}, %
publisher = {Springer}, %
year = {1990} %
}%
J. Woodcock, C. C. Morgan, What is a Specification? in Dan Craigen
(ed.) and Karen Summerskill (assistant ed.), Formal Methods for Trustworthy
Computer Systems (FM89), Workshops in Computing Series, Springer, 1990.
pp.33-37.
@incollection{%
chapter:WoodcockMorgan90, %
author = {J. Woodcock and C. C.
Morgan}, %
title = {What is a Specification?},
%
editor = {Dan Craigen and Karen
Summerskill}, %
booktitle = {Formal Methods for Trustworthy Computer
Systems (FM89)}, %
series = {Workshops in Computing
Series}, %
publisher = {Springer}, %
year = {1990}, %
pages = {33--37} %
}%
S. Brien, J. Woodcock, Semantic Metalanguage, Semantic Universe,
Expression, Predicate, Declaration, Schema, A Deductive System for Z, (7
chapters) in Z Base Standard Version 1.0, Technical Monograph PRG-107. Oxford
University Programming Research Group, Nov 1992.
@incollection{%
chapter:BrienWoodcock92, %
author = {S. Brien and J. Woodcock},
%
title = {Semantic Metalanguage,
Semantic Universe, Expression, Predicate, Declaration, Schema, A Deductive
System for Z}, %
booktitle = {Z Base Standard Version 1.0}, %
series = {Technical Monograph},
%
number = {PRG-107}, %
chapter = {1--7}, %
publisher = {Oxford University Programming Research
Group}, %
month = {November}, %
year = {1992} %
}%
chapter:WoodcockDaviesBolton00
J. Woodcock, J. Davies, C. Bolton, Abstract Data Types and
Processes, in J. Davies, A. W. Roscoe, and J. Woodcock, (eds), Proceedings of
the Symposium in Honour of C. A. R. Hoare, Palgrave, 2000. pp.391-405.
@incollection{%
chapter:WoodcockDaviesBolton00, %
author = {J. Woodcock and J. Davies
and C. Bolton}, %
title = {Abstract Data Types
and Processes}, %
editor = {J. Davies and A. W.
Roscoe and J. Woodcock}, %
booktitle = {Proceedings of the Symposium in Honour
of C. A. R. Hoare}, %
publisher = {Palgrave}, %
year = {2000}, %
pages = {391--405} %
}%
J. Woodcock, Unifying Theories of Parallel Programming, in Logic
and Algebra for Engineering Software, IOS Press, 2003.
@incollection{%
chapter:Woodcock03, %
author = {J. Woodcock}, %
title = {Unifying Theories
of Parallel Programming}, %
booktitle = {Logic and Algebra for Engineering Software},
%
publisher = {IOS Press}, %
year = {2003} %
}%
chapter:CavalcantiSampaioWoodcock06
A. Cavalcanti, A. Sampaio and J. Woodcock, Refinement: An Overview,
in Refinement Techniques in Software Engineering, LNCS
3167, 2006.
@inproceedings{%
chapter:CavalcantiSampaioWoodcock06, %
author = {A. Cavalcanti and
A. Sampaio and J. Woodcock}, %
title = {Refinement: An
Overview}, %
booktitle = {Refinement Techniques in Software Engineering},
%
series = {LNCS}, %
volume = {3167}, %
publisher = {Springer}, %
year = {2006} %
}%
A. Cavalcanti, J. Woodcock, A Tutorial Introduction to CSP in
Unifying Theories of Programming, in Refinement Techniques in Software
Engineering LNCS 3167, pp.220–268, Springer, 2006.
@incollection{%
chapter:CavalcantiWoodcock06, %
author = {A. Cavalcanti and J.
Woodcock}, %
title = {A Tutorial Introduction
to CSP in Unifying Theories of Programming}, %
booktitle = {Refinement Techniques in Software Engineering},
%
series = {LNCS}, %
volume = {3167}, %
pages = {220--268}, %
publisher = {Springer}, %
year = {2006} %
}%
L. Freitas, J. Woodcock. Proving Theorems about JML Classes. Essays
in Honour of Dines Bjørner and Zhou Chaochen on the Occasion of their 70th
Birthdays, Papers presented at a Symposium held in Macao on 24th & 25th
Sep 2007. LNCS 4700, Springer, 2007.
@inproceedings{%
chapter:FreitasWoodcock07, %
author = {Leo Freitas and Jim
Woodcock}, %
title = {Proving Theorems
About JML Classes}, %
booktitle = {Formal Methods and Hybrid Real-Time
Systems}, %
year = {2007}, %
pages = {255-279}, %
ee = {http://dx.doi.org/10.1007/978-3-540-75221-9\_11},
%
crossref = {proceedings:JonesLiuWoodcock},
%
}%
J. Woodcock, Z Logic and its Applications, in D. Bjørner, M. Henson
(eds), Logics of Formal Specification Languages,
Springer, 2007.
@incollection{%
chapter:Woodcock07, %
author = {J. Woodcock}, %
title = {Z Logic and its
Applications}, %
editor = {D. Bj{\o}rner and M.
Henson}, %
booktitle = {Logics of Formal Specification Languages},
%
publisher = {Springer}, %
year = {2007} %
}%
Journal papers
J. Woodcock, Software specification and design for the VLSI era, GEC
Journal of Science & Technology 48(2):86–89 1982.
@article{%
journal:Woodcock82, %
author = {J. Woodcock}, %
title = {Software specification
and design for the VLSI era}, %
journal = {GEC Journal of Science \&
Technology}, %
volume = {48}, %
number = {2}, %
pages = {86--89}, %
year = {1982} %
}%
J. Woodcock, The formal specification of a lift system in Milner’s
CCS, Software Engineering Journal May 1987.
@article{%
journal:Woodcock87a, %
author = {J. Woodcock}, %
title = {The formal specification
of a lift system in Milner’s CCS}, %
journal = {Software Engineering Journal},
%
month = {May}, %
year = {1987} %
}%
J. Woodcock, Towards the formal specification of a programming
support environment, Software Engineering Journal Jul 1987.
@article{%
journal:Woodcock87b, %
author = {J. Woodcock}, %
title = {Towards the formal
specification of a programming support environment}, %
journal = {Software Engineering Journal},
%
month = {July}, %
year = {1987} %
}%
J. Woodcock, Transaction processing primitives and CSP, IBM
Journal of Research & Development 31(5):535–545 1987.
@article{%
journal:Woodcock87c, %
author = {J. Woodcock}, %
title = {Transaction processing
primitives and CSP}, %
journal = {IBM Journal of Research \&
Development}, %
volume = {31}, %
number = {5}, %
pages = {535--545}, %
year = {1987} %
}%
J. Woodcock, Structuring specifications in Z, Software Engineering
Journal Jul 1988.
@article{%
journal:Woodcock88, %
author = {J. Woodcock}, %
title = {Structuring specifications
in Z}, %
journal = {Software Engineering Journal},
%
month = {July}, %
year = {1988} %
}%
J. Woodcock, Formal techniques and operational specifications,
Software Engineering Notes 14 1989.
@article{%
journal:Woodcock89, %
author = {J. Woodcock}, %
title = {Formal techniques
and operational specifications}, %
journal = {Software Engineering Notes},
%
volume = {14}, %
year = {1989} %
}%
J. Woodcock, The rudiments of algorithm refinement, Computer
Journal 35(5):441–450 1992.
@article{%
journal:Woodcock92, %
author = {Jim Woodcock}, %
title = {The Rudiments of
Algorithm Refinement}, %
journal = {Comput. J.}, %
volume = {35}, %
number = {5}, %
year = {1992}, %
pages = {441-450}, %
}%
J. Sinclair, J. Woodcock, Event refinement in state-based
concurrent systems, Formal Aspects of Computing Journal 7(3):266–288 1995.
@article{%
journal:SinclairWoodcock95, %
author = {Jane Sinclair and Jim
Woodcock}, %
title = {Event Refinement
in State-Based Concurrent Systems}, %
journal = {Formal Asp. Comput.}, %
volume = {7}, %
number = {3}, %
year = {1995}, %
pages = {266-288}, %
}%
J. Woodcock, P. Larsen, Introduction to special section (Guest
Editorial), IEEE Transactions on Software Engineering 21(2):61–62
1995.
@article{%
journal:WoodcockLarsen95, %
author = {Jim Woodcock and Peter
Gorm Larsen}, %
title = {Introduction to
Special Section (Guest Editorial)}, %
journal = {IEEE Trans. Software Eng.},
%
volume = {21}, %
number = {2}, %
year = {1995}, %
pages = {61-62}, %
ee = {http://www.computer.org/tse/ts1995/e0061abs.htm},
%
}%
@article{%
journal:Woodcock96, %
author = {Jim Woodcock}, %
title = {Software Engineering
Research Directions}, %
journal = {ACM Comput. Surv.}, %
volume = {28}, %
number = {4es}, %
year = {1996}, %
pages = {128}, %
}%
E. M. Clark, J. Wing, J. Woodcock, et al, Formal methods: state of
the art and future directions, ACM Computing Surveys 28(4):626–643
1996.
@article{%
journal:ClarkWingWoodcock, %
author = {Edmund M. Clark and
Jeannette M. Wing and Jim Woodcock}, %
title = {Formal Methods:
State of the Art and Future Directions}, %
journal = {ACM Comput. Surv.}, %
volume = {28}, %
number = {4}, %
year = {1996}, %
pages = {626-643}, %
}%
journal:MartinGardinerWoodcock96
A. P. Martin, P. H. B. Gardiner, J. Woodcock, A tactic
calculus—abridged version, Formal Aspects of Computing Journal 8(4):479–489
1996.
@article{%
journal:MartinGardinerWoodcock96, %
author = {A. P. Martin and Paul
H. B. Gardiner and Jim Woodcock}, %
title = {A Tactic Calculus-Abridged
Version}, %
journal = {Formal Asp. Comput.}, %
volume = {8}, %
number = {4}, %
year = {1996}, %
pages = {479-489}, %
}%
A. W. Roscoe, J. Woodcock, L. Wulf, Non-interference through
determinism, Journal of Computer Security 4(1):27–54 1996.
@article{%
journal:RoscoeWoodcockWulf96, %
author = {A. W. Roscoe and Jim
Woodcock and L. Wulf}, %
title = {Non-interference
through Determinism}, %
journal = {Journal of Computer Security},
%
volume = {4}, %
number = {1}, %
year = {1996}, %
pages = {27-54}, %
}%
journal:CavalcantiSampaioWoodcock98
A. Cavalcanti, A. Sampaio, J. Woodcock, Procedures and recursion in
the refinement calculus, Journal of the Brazilian Computer Society 5(1):1–15
1998.
@article{%
journal:CavalcantiSampaioWoodcock98, %
author = {Ana Cavalcanti and Augusto
Sampaio and Jim Woodcock}, %
title = {Procedures and
Recursion in the Refinement Calculus}, %
journal = {J. Braz. Comp. Soc.}, %
volume = {5}, %
number = {1}, %
year = {1998}, %
}%
A. Cavalcanti, J. Woodcock, A weakest precondition semantics for Z,
Computer Journal 41(1):1–15 1998.
@article{%
journal:CavalcantiWoodcock98a, %
author = {Ana Cavalcanti and Jim
Woodcock}, %
title = {A Weakest Precondition
Semantics for Z}, %
journal = {Comput. J.}, %
volume = {41}, %
number = {1}, %
year = {1998}, %
pages = {1-15}, %
}%
A. Cavalcanti, J. Woodcock, ZRC—a refinement calculus for Z, Formal
Aspects of Computing Journal 10(3):267–289 1998.
@article{%
journal:CavalcantiWoodcock98b, %
author = {Ana Cavalcanti and Jim
Woodcock}, %
title = {ZRC - A Refinement
Calculus for Z}, %
journal = {Formal Asp. Comput.}, %
volume = {10}, %
number = {3}, %
year = {1998}, %
pages = {267-289}, %
ee = {http://link.springer.de/link/service/journals/00165/bibs/8010003/80100267.htm},
%
}%
journal:CavalcantiSampaioWoodcock99
A. Cavalcanti, A. Sampaio, J. Woodcock, An inconsistency in
procedures, parameters, and substitution in the refinement calculus, Science of
Computer Programming 33(1):87–96 1999.
@article{%
journal:CavalcantiSampaioWoodcock99, %
author = {Ana Cavalcanti and Augusto
Sampaio and Jim Woodcock}, %
title = {An Inconsistency
in Procedures, Parameters, and Substitution in the Refinement Calculus}, %
journal = {Sci. Comput. Program.}, %
volume = {33}, %
number = {1}, %
year = {1999}, %
pages = {87-96}, %
}%
J. Wing, J. Woodcock, Introduction: Special Issues for FM’99: the
First World Congress on Formal Methods in the Development of Computing Systems,
Guest eds, Formal Aspects of Computing Journal 12(3):145–146 2000.
@article{%
journal:WingWoodcock00a, %
author = {Jeannette M. Wing and
Jim Woodcock}, %
title = {The First World
Congress on Formal Methods in the Development of Computing Systems}, %
journal = {Formal Asp. Comput.}, %
volume = {12}, %
number = {3}, %
year = {2000}, %
pages = {145-146}, %
ee = {http://link.springer.de/link/service/journals/00165/bibs/0012003/00120145.htm},
%
}%
J. Wing, J. Woodcock, 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(3): 199–200 (2000).
@article{%
journalWingWoodcock00b, %
author = {Jeannette M. Wing and
Jim Woodcock}, %
title = {Introduction: Special
Issues for FM'99, the First World Congress on Formal Methods in the Development
of Computing Systems}, %
journal = {Formal Methods in System
Design}, %
volume = {17}, %
number = {3}, %
year = {2000}, %
pages = {199-200}, %
}%
J. Wing, J. Woodcock, Introduction: Special Issues for FM’99: the
First World Congress on Formal Methods in the Development of Computing Systems,
Guest eds, IEEE Transactions on Software Engineering 26(8)673–674
Aug 2000.
@article{%
journal:WingWoodcock00c, %
author = {Jeannette M. Wing and
Jim Woodcock}, %
title = {Guest Editors'
Introduction-Special Issues for FM '99: The First World Congress On Formal Methods
in the Development of Computing Systems}, %
journal = {IEEE Trans. Software Eng.},
%
volume = {26}, %
number = {8}, %
year = {2000}, %
pages = {673-674}, %
ee = {http://dlib.computer.org/ts/books/ts2000/pdf/e0673.pdf},
%
}%
journal:CavalcantiSampaioWoodcock03
A. Cavalcanti, A. Sampaio, J. Woodcock, A refinement strategy for
Circus, Formal Aspects of Computing Journal 15(2–3):146–181, 2003.
@article{%
journal:CavalcantiSampaioWoodcock03, %
author = {Ana Cavalcanti and Augusto
Sampaio and Jim Woodcock}, %
title = {A Refinement Strategy
for Circus}, %
journal = {Formal Asp. Comput.}, %
volume = {15}, %
number = {2-3}, %
year = {2003}, %
pages = {146-181}, %
ee = {http://dx.doi.org/10.1007/s00165-003-0006-5},
%
}%
A. Cavalcanti, J. Woodcock Predicate transformers in the semantics
of Circus, IEE Proceedings Software 150(1):85–94 2003.
@article{%
journal:CavalcantiWoodcock03, %
author = {Ana Cavalcanti and Jim
Woodcock}, %
title = {Predicate transformers
in the semantics of Circus}, %
journal = {IEE Proceedings - Software},
%
volume = {150}, %
number = {2}, %
year = {2003}, %
pages = {85-94}, %
}%
journal:OliveiraCavalcantiWoodcock03
M. Oliveira, A. Cavalcanti, J. Woodcock, ArcAngel: a tactic
language for refinement, Formal Aspects of Computing Journal 15(1):28–47 2003.
@article{%
journalOliveiraCavalcantiWoodcock03, %
author = {Marcel Oliveira and
Ana Cavalcanti and Jim Woodcock}, %
title = {ArcAngel: a Tactic
Language for Refinement}, %
journal = {Formal Asp. Comput.}, %
volume = {15}, %
number = {1}, %
year = {2003}, %
pages = {28-47}, %
ee = {http://dx.doi.org/10.1007/s00165-003-0003-8},
%
}%
A. Butterfield, J. Woodcock, prialt in Handel-C: an operational
semantics, International Journal on Software Tools for Technology Transfer 7(3):248–267
2005.
@article{%
journal:ButterfieldWoodcock05, %
author = {Andrew Butterfield and
Jim Woodcock}, %
title = {prialt in Handel-C:
an operational semantics}, %
journal = {STTT}, %
volume = {7}, %
number = {3}, %
year = {2005}, %
pages = {248-267}, %
ee = {http://dx.doi.org/10.1007/s10009-004-0181-6},
%
}%
journal:CavalcantiSampaioWoodcock05
A. Cavalcanti, A. Sampaio, J. Woodcock, Unifying classes and
processes, Software and System Modeling 4(3):277–296 2005.
@article{%
journal:CavalcantiSampaioWoodcock, %
author = {Ana Cavalcanti and Augusto
Sampaio and Jim Woodcock}, %
title = {Unifying classes
and processes}, %
journal = {Software and System Modeling},
%
volume = {4}, %
number = {3}, %
year = {2005}, %
pages = {277-296}, %
ee = {http://dx.doi.org/10.1007/s10270-005-0085-2},
%
}%
journal:OliveiraCavalcantiWoodcock05
M. Oliveira, A. Cavalcanti, J. Woodcock, Formal development of
industrial-scale systems Circus, Innovations in Systems and Software
Engineering 1(2):125–146 2005.
@article{%
journal:OliveiraCavalcantiWoodcock05, %
author = {M. Oliveira and A. Cavalcanti
and J. Woodcock}, %
title = {Formal development
of industrial-scale systems Circus}, %
journal = {Innovations in Systems and
Software Engineering}, %
volume = {1}, %
number = {2}, %
pages = {125--146}, %
year = {2005} %
}%
journal:BicarreguiHoareWoodcock06
Juan Bicarregui, C. A. R. Hoare, J. Woodcock, The verified software
repository: a step towards the verifying compiler, Formal Aspects of Computing
Journal 18(2):143–151 2006.
@article{%
journal:BicarreguiHoareWoodcock06, %
author = {Juan Bicarregui and
C. A. R. Hoare and J. C. P. Woodcock}, %
title = {The verified software
repository: a step towards the verifying compiler}, %
journal = {Formal Asp. Comput.}, %
volume = {18}, %
number = {2}, %
year = {2006}, %
pages = {143-151}, %
ee = {http://dx.doi.org/10.1007/s00165-005-0079-4},
%
}%
journal:CavalcantiWoodcockDunne06
A. Cavalcanti, J. Woodcock, S. Dunne, Angelic nondeterminism in the
unifying theories of programming, Formal Aspects of Computing Journal
18(3):288–307 2006.
@article{%
journal:CavalcantiWoodcockDunne06, %
author = {Ana Cavalcanti and Jim
Woodcock and Steve Dunne}, %
title = {Angelic nondeterminism
in the unifying theories of programming}, %
journal = {Formal Asp. Comput.}, %
volume = {18}, %
number = {3}, %
year = {2006}, %
pages = {288-307}, %
ee = {http://dx.doi.org/10.1007/s00165-006-0001-8},
%
}%
journal:FreitasWoodcockCavalcanti06
L. Freitas, J. Woodcock, A. Cavalcanti, State-rich model checking, Innovations
in Systems and Software Engineering 2(1) 2006.
@article{%
journal:FreitasWoodcockCavalcanti06, %
author = {L. Freitas and J. Woodcock
and A. Cavalcanti}, %
title = {State-rich model
checking}, %
journal = {Innovations in Systems and
Software Engineering}, %
volume = {2}, %
number = {1}, %
year = {2006} %
}%
C. Jones, P. W. O’Hearn, J. Woodcock, Verified software: a grand
challenge, IEEE Computer 39(4):93–95 2006.
@article{%
journal:JonesOHearnWoodcock06, %
author = {Cliff B. Jones and Peter
W. O'Hearn and Jim Woodcock}, %
title = {Verified Software:
A Grand Challenge}, %
journal = {IEEE Computer}, %
volume = {39}, %
number = {4}, %
year = {2006}, %
pages = {93-95}, %
ee = {http://doi.ieeecomputersociety.org/10.1109/MC.2006.145},
%
}%
journal:OliveiraCavalcantiWoodcock07
M. Oliveira, A. Cavalcanti, J. Woodcock, Unifying theories in
ProofPower-Z, Formal Aspects of Computing Journal 2006.
@article{%
journal:OliveiraCavalcantiWoodcock07, %
author = {M. Oliveira and A. Cavalcanti
and J. Woodcock}, %
title = {Unifying theories
in ProofPower-Z}, %
journal = {Formal Aspects of Computing
Journal}, %
year = {2007} %
}%
J. Woodcock, First steps in the Verified Software Grand Challenge,
IEEE Computer 39(10): 57–64 2006.
@article{%
journal:Woodcock06, %
author = {Jim Woodcock}, %
title = {First Steps in
the Verified Software Grand Challenge}, %
journal = {IEEE Computer}, %
volume = {39}, %
number = {10}, %
year = {2006}, %
pages = {57-64}, %
ee = {http://doi.ieeecomputersociety.org/10.1109/MC.2006.340},
%
}%
J. Woodcock, Richard Banach, The Verification Grand Challenge, Computer
Society of India Communications 31(2):33–36 2007.
@article{%
journal:WoodcockBanach07a, %
author = {J. Woodcock and Richard
Banach}, %
title = {The Verification
Grand Challenge}, %
journal = {Computer Society of India
Communications}, %
volume = {31}, %
number = {2}, %
pages = {:33--36}, %
year = {2007} %
}%
J. Woodcock, Richard Banach, The Verification Grand Challenge, Journal
of Universal Computer Science 13(5):661–668 2007.
@article{%
journal:WoodcockBanach07b, %
author = {J. Woodcock and Richard
Banach}, %
title = {The Verification
Grand Challenge}, %
journal = {Journal of Universal Computer
Science}, %
volume = {13}, %
number = {5}, %
pages = {661--668}, %
year = {2007} %
}%
journal:WoodcockCavalcantiGaudelFreitas07
J. Woodcock, A. Cavalcanti, M.-C. Gaudel, L. Freitas, Circus
operational semantics, Formal Aspects of Computing Journal, in press 2007.
@article{%
journal:WoodcockCavalcantiGaudelFreitas07, %
author = {J. Woodcock and A. Cavalcanti
and M.-C. Gaudel and L. Freitas}, %
title = {Circus operational
semantics}, %
journal = {Formal Aspects of Computing
Journal}, %
year = {2007} %
}%
journal:ButterfieldFreitasWoodcock08
A. Butterfield, J. Woodcock, A mechanised model of NAND flash
memory, Science of Computer Programming in press 2008.
@article{%
journal:ButterfieldFreitasWoodcock08, %
author = {A. Butterfield and Freitas
and J. Woodcock}, %
title = {A mechanised model
of NAND flash memory}, %
journal = {Science of Computer Programming},
%
year = {2008} %
}%
L. Freitas, Z. Fu, J. Woodcock, A mechanically verified
specification and refinement of the POSIX file-store interface,
Science of Computer Programming in press 2008.
@article{%
journal:FreitasFuWoodcock08, %
author = {L. Freitas and Z. Fu
and J. Woodcock}, %
title = {A mechanically
verified specification and refinement of the POSIX file-store interface}, %
journal = {Science of Computer Programming},
%
year = {2008} %
}%
journal:FreitasMokosWoodcock08
L. Freitas, K. Mokos, J. Woodcock, A mechanical verification of the
CICS File Control API, Science of Computer Programming in press 2008.
@article{%
journal:FreitasMokosWoodcock08, %
author = {L. Freitas and K. Mokos
and J. Woodcock}, %
title = {A mechanical verification
of the CICS File Control API}, %
journal = {Science of Computer Programming},
%
year = {2008} %
}%
L. Freitas, J. Woodcock, Mechanising Mondex with Z/EVES, Formal
Aspects of Computing Journal 20(1) 2008.
@article{%
journal:FreitasWoodcock08a, %
author = {L. Freitas and J. Woodcock},
%
title = {Mechanising Mondex
with Z/EVES}, %
journal = {Formal Aspects of
Computing Journal}, %
volume = {20}, %
number = {1}, %
year = {2008} %
}%
L. Freitas, J. Woodcock, FDR Explorer, Formal Aspects of Computing
Journal 20(2) 2008.
@article{%
journal:FreitasWoodcock08b, %
author = {L. Freitas and J. Woodcock},
%
title = {FDR Explorer},
%
journal = {Formal Aspects of Computing
Journal}, %
volume = {20}, %
number = {2}, %
year = {2008} %
}%
journal:WoodcockStepneyCooperClarkJacob
J. Woodcock, S. Stepney, D. Cooper, J. Clark, J. Jacob, The
certification of the Mondex electronic purse to ITSEC Level E6, Formal Aspects
of Computing 20(1) 2008.
@article{%
journal:WoodcockStepneyCooperClarkJacob, %
author = {J. Woodcock and S. Stepney
and D. Cooper and J. Clark and J. Jacob}, %
title = {The certification
of the Mondex electronic purse to ITSEC Level E6}, %
journal = {Formal Aspects of Computing},
%
volume = {20}, %
number = {1}, %
year = {2008} %
}%
J. Woodcock, Formal specification in industry, in R. Babb and A.
Mili (eds), Workshop Notes, IEEE International Workshop on Models and Languages
for Software Specification and Design, Orlando, Florida, IEEE Press,
1984. Invited paper.
@inproceedings{%
conference:Woodcock84, %
author = {J. Woodcock}, %
title = {Formal specification
in industry}, %
editor = {R. Babb and A. Mili},
%
booktitle = {Workshop Notes, IEEE International
Workshop on Models and Languages for Software Specification and Design, Orlando,
Florida}, %
publisher = {IEEE Press}, %
year = {1984} %
}%
J. Woodcock Formal methods for program specification and
verification, in M. Hennell (ed.), Workshop Notes, 3rd IEEE International
Workshop on Software Specification and Design, London, IEEE Press,
1985.
@inproceedings{%
conference:Woodcock85, %
author = {J. Woodcock}, %
title = {Formal methods
for program specification and verification}, %
editor = {M. Hennell}, %
booktitle = {Workshop Notes, 3rd IEEE International
Workshop on Software Specification and Design, London}, %
publisher = {IEEE Press}, %
year = {1985} %
}%
J. Woodcock, Formal specification of the lift problem, in M.
Harandi (ed.), Workshop Notes, 4th IEEE International Workshop on Software Specification
and Design, Monterey, California, IEEE Press, 1987.
@inproceedings{%
conference:Woodcock87, %
author = {J. Woodcock}, %
title = {Formal specification
of the lift problem}, %
editor = {M. Harandi}, %
booktitle = {Workshop Notes, 4th IEEE International
Workshop on Software Specification and Design, Monterey, California}, %
publisher = {IEEE Press}, %
year = {1987} %
}%
conference:WoodcockDickinson88
J. Woodcock, B. Dickinson, Using VDM with rely and
guarantee-conditions — Experiences from a real project, in R. Bloomfield, L.
Marshall, R. Jones (eds), VDM’88: VDM—The Way Ahead. Proceedings of the 2nd
VDM-Europe Symposium 1988, LNCS 328:434-458. Springer, 1988.
@inproceedings{%
conference:WoodcockDickinson88, %
author = {Jim Woodcock and B.
Dickinson}, %
title = {Using VDM with
Rely and Guarantee-Conditions - Experiences from a Real Project}, %
booktitle = {VDM Europe}, %
year = {1988}, %
pages = {434-458}, %
crossref = {proceedings:BloomfieldMarshallJones88}
%
}%
J. Woodcock, Calculating properties of Z specifications, Proceedings
of the 5th IEEE International Workshop on Software Specification and Design,
Pittsburgh, 1989.
@inproceedings{%
conference:Woodcock89, %
author = {J. Woodcock}, %
title = {Calculating properties
of Z specifications}, %
booktitle = {Proceedings of the 5th IEEE International
Workshop on Software Specification and Design, Pittsburgh}, %
publisher = {IEEE Press}, %
year = {1989} %
}%
conference:GardinerLuptonWoodcock90
P. H. B. Gardiner, P. J. Lupton, J. Woodcock, A simpler semantics
for Z, J. Nicholls (ed.), Z User Workshop,
Oxford 1990, Workshops in Computing series, pp.3–11, Springer, 1990.
@inproceedings{%
conference:GardinerLuptonWoodcock90, %
author = {Paul H. B. Gardiner
and P. J. Lupton and Jim Woodcock}, %
title = {A Simpler Semantics
for Z}, %
booktitle = {Z User Workshop}, %
year = {1990}, %
pages = {3-11}, %
crossref = {proceedings:Nicholls91}, %
}%
@proceedings{%
proceedings:Nicholls91, %
editor = {J. E. Nicholls}, %
title = {Z User Workshop,
Oxford, UK, Proceedings of the Fifth Annual Z User Meeting, 17-18 December 1990},
%
booktitle = {Z User Workshop}, %
publisher = {Springer}, %
series = {Workshops in Computing},
%
year = {1991}, %
isbm = {3-540-19672-2},
%
}%
J. Woodcock, C. Morgan, Refinement of state-based concurrent
systems, D. Bjørner, C. A. R. Hoare, and H. Langmaack (eds), VDM’90: VDM and
Z—Formal Methods in Software Development. Third International Symposium of VDM
Europe, LNCS 428:340-351, Springer, 1990.
@inproceedings{%
conference:WoodcockMorgan90, %
author = {Jim Woodcock and Carroll
Morgan}, %
title = {Refinement of State-Based
Concurrent Systems}, %
booktitle = {VDM Europe}, %
year = {1990}, %
pages = {340-351}, %
crossref = {proceedings:BjornerHoareLangmaack90},
%
}%
proceedings:BjornerHoareLangmaack90
@proceedings{%
proceedings:BjornerHoareLangmaack90, %
editor = {Dines Bj{\o}rner and
C. A. R. Hoare and Hans Langmaack}, %
title = {VDM '90, VDM and
Z - Formal Methods in Software Development, Third International Symposium of
VDM Europe, Kiel, FRG, April 17-21, 1990, Proceedings}, %
booktitle = {VDM Europe}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {428}, %
year = {1990}, %
isbm =
{3-540-52513-0}, %
}%
J. Woodcock, An introduction to refinement in Z, in S. Prehn and W.
J. Toetenel (eds), VDM’91: Formal Software Development Methods. 4th
International Symposium of VDM Europe, LNCS 552:96–117. Springer, 1991.
@inproceedings{%
conference:Woodcock91a, %
author = {Jim Woodcock}, %
title = {An Introduction
to Refinement in Z}, %
booktitle = {VDM Europe (2)}, %
year = {1991}, %
pages = {96-117}, %
crossref = {proceedings:PrehnToetenel91},
%
}%
@proceedings{%
proceedings:PrehnToetenel91, %
editor = {S{\o}ren Prehn and W.
J. Toetenel}, %
title = {VDM '91 - Formal
Software Development, 4th International Symposium of VDM Europe, Noordwijkerhout,
The Netherlands, October 21-25, 1991, Proceedings, Volume 2: Tutorials}, %
booktitle = {VDM Europe (2)}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {552}, %
year = {1991}, %
isbm = {3-540-54868-8},
%
}%
J. Woodcock, The refinement calculus, in S. Prehn and W. J.
Toetenel (eds), VDM’91: Formal Software Development Methods. 4th International
Symposium of VDM Europe, LNCS 552:80–95, Springer, 1991.
@inproceedings{%
conference:Woodcock91b, %
author = {Jim Woodcock}, %
title = {The Refinement
Calculus}, %
booktitle = {VDM Europe (2)}, %
year = {1991}, %
pages = {80-95}, %
crossref = {proceedings:PrehnToetenel91},
%
}%
J. Woodcock, Two refinement case studies, in S. Prehn and W. J.
Toetenel (eds), VDM’91: Formal Software Development Methods. 4th International
Symposium of VDM Europe, LNCS 552:118– 140, Springer, 1991.
@inproceedings{%
conference:Woodcock91c, %
author = {Jim Woodcock}, %
title = {Two Refinement
Case Studies}, %
booktitle = {VDM Europe (2)}, %
year = {1991}, %
pages = {118-140}, %
crossref = {proceedings:PrehnToetenel91},
%
}%
@inproceedings{%
conference:Woodcock91d, %
author = {Jim Woodcock}, %
title = {A Tutorial on the
Refinement Calculus}, %
booktitle = {VDM Europe (2)}, %
year = {1991}, %
pages = {79-140}, %
crossref = {proceedings:PrehnToetenel91},
%
}%
J. Woodcock, S. Brien, W: a logic for Z, Z User Workshop, York
1991, Workshop in Computing Series, pp.77–998, Springer, 1991.
@inproceedings{%
conference:WoodcockBrien91, %
author = {J. Woodcock and S. Brien},
%
title = {W: a logic for
Z}, %
booktitle = {Z User Workshop, York 1991}, %
series = {Workshop in Computing
Series}, %
pages = {77--998}, %
publisher = {Springer}, %
year = {1991} %
}%
J. Woodcock, Implementing promoted operations in Z, in C. Jones, R.
Shaw, T. Denvir (eds), 5th Refinement Workshop, Workshops in Computing Series,
pp.367–378, Springer, 1992.
@proceedings{%
conference:Woodcock92, %
author = {J. Woodcock}, %
title = {Implementing promoted
operations in Z}, %
editor = {C. Jones and R. Shaw
T. Denvir}, %
booktitle = {5th Refinement Workshop}, %
series = {Workshops in Computing
Series}, %
pages = {367--378}, %
publisher = {Springer}, %
year = {1992} %
}%
conference:RoscoeWoodcockWulf94
A. W. Roscoe, J. Woodcock, L. Wulf, Non-interference through
determinism, in D. Gollman (ed.), Computer Security—ESORICS’94. Third European
Symposium on Research in Computer Security, Brighton, LNCS 875:33–54, Springer,
1994.
@inproceedings{%
conference:RoscoeWoodcockWulf94, %
author = {A. W. Roscoe and Jim
Woodcock and L. Wulf}, %
title = {Non-Interference
Through Determinism}, %
booktitle = {ESORICS}, %
year = {1994}, %
pages = {33-53}, %
ee = {http://dx.doi.org/10.1007/3-540-58618-0\_55},
%
crossref = {proceedings:Gollman94}, %
}%
@proceedings{%
proceedings:Gollman94, %
editor = {Dieter Gollmann}, %
title = {Computer Security
- ESORICS 94, Third European Symposium on Research in Computer Security,Typeon,
UK, November 7-9, 1994, Proceedings}, %
booktitle = {ESORICS}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {875}, %
year = {1994}, %
isbm = {3-540-58618-0},
%
}%
conference:WoodcockGardinerHulance94
J. Woodcock, P. H. B. Gardiner, J. Hulance, The formal
specification in Z of Defence Standard 00–56, in J. P. Bowen and J. A. Hall
(eds), Z User Workshop, Cambridge 1994. Workshop in Computing series, pp.9–28,
Springer, 1994. Keynote speech.
@inproceedings{%
conference:WoodcockGardinerHulance94, %
author = {Jim Woodcock and Paul
H. B. Gardiner and J. R. Hulance}, %
title = {The Formal Specification
in Z of Defence Standard 00-56}, %
booktitle = {Z User Workshop}, %
year = {1994}, %
pages = {9-28}, %
}%
conference:SimpsonWoodcockDavies97
A. Simpson, J. Woodcock, J. Davies, The mechanical verification of
solid-state interlocking geographic data, in J. Grundy, M. Schwenke, T. Vickers
(eds), Formal Methods Pacific ’97, pp.223– 243, Springer, 1997.
@inproceedings{%
conference:SimpsonWoodcockDavies97, %
author = {A. Simpson and J. Woodcock
and J. Davies}, %
title = {The mechanical
verification of solid-state interlocking geographic data}, %
editor = {J. Grundy and M. Schwenke
and T. Vickers}, %
booktitle = {Formal Methods Pacific ’97}, %
pages = {223--243}, %
publisher = {Springer}, %
year = {1997} %
}%
conference:SimpsonDaviesWoodcock98a
A. Simpson, J. Davies, J. Woodcock, Security management via Z and
CSP, in J. Grundy, M. Schwenke, T. Vickers (eds), Formal Methods Pacific
’98/International Refinement Workshop ’98, Springer Series in Discrete
Mathematics and Theoretical Computer Science, pp.334–351, 1998.
@inproceedings{%
conference:SimpsonDaviesWoodcock98a, %
author = {A. Simpson and J. Davies
and J. Woodcock}, %
title = {Security management
via Z and CSP}, %
editor = {J. Grundy and M. Schwenke
and T. Vickers}, %
booktitle = {Formal Methods Pacific ’98/International
Refinement Workshop ’98}, %
publisher = {Springer}, %
series = {Series in Discrete Mathematics
and Theoretical Computer Science}, %
pages = {334--351}, %
year = {1998} %
}%
conference:SimpsonWoodcockDavies98
A. Simpson, J. Woodcock, J. Davies, Safety through security, Proceedings
of the 9th IEEE International Workshop on Software Specification and Design,
Ise-Shima, Japan, IEEE Computer Society Press, pp.18–24, 1998.
@inproceedings{%
conference:SimpsonDaviesWoodcock98b, %
author = {A. Simpson and J. Woodcock
and J. Davies}, %
title = {Safety through
security}, %
booktitle = {Proceedings of the 9th IEEE International
Workshop on Software Specification and Design, Ise-Shima, Japan}, %
publisher = {IEEE Computer Society Press}, %
pages = {18--24}, %
year = {1998} %
}%
conference:StepneyCooperWoodcock98
S. Stepney, D. Cooper, J. Woodcock, More powerful Z data
refinement: pushing the state of the art in industrial refinement, in J. P.
Bowen, A. Fett, M. G. Hinchey (eds), 11th International Conference of
Z Users, Berlin. Sep 1998. LNCS 1493:284–307, Springer, 1998. Winner of
the best paper award.
@inproceedings{%
conference:StepneyCooperWoodcock98, %
author = {Susan Stepney and David
Cooper and Jim Woodcock}, %
title = {More Powerful Z
Data Refinement: Pushing the State of the Art in Industrial Refinement}, %
booktitle = {ZUM}, %
year = {1998}, %
pages = {284-307}, %
crossref = {proceedings:BowenFettHinchey98},
%
}%
proceedings:BowenFettHinchey98
J. Woodcock, Industrial-strength refinement, Proceedings of the
Joint Formal Methods Pacific ’98/International Refinement Workshop ’98 and
Conference on Theorem Proving in Higher-Order Logics, Canberra, Australia, Sep 1998,
Springer Series in Discrete Mathematics and Theoretical Computer Science,
pp.33–44, 1998. Keynote speech.
@proceedings{%
proceedings:BowenFettHinchey98, %
editor = {Jonathan P. Bowen and
Andreas Fett and Michael G. Hinchey}, %
title = {ZUM '98: The Z
Formal Specification Notation, 11th International Conference of Z Users, Berlin,
Germany, September 24-26, 1998, Proceedings}, %
booktitle = {ZUM}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {1493}, %
year = {1998}, %
isbm = {3-540-65070-9}
%
}%
J. Woodcock, Industrial-strength refinement, Proceedings of the
Joint Formal Methods Pacific ’98/International Refinement Workshop ’98 and
Conference on Theorem Proving in Higher-Order Logics, Canberra, Australia, Sep
1998, Springer Series in Discrete Mathematics and Theoretical Computer Science,
pp.33–44, 1998. Keynote speech.
@inproceedings{%
conference:woodcock98, %
author = {J. Woodcock}, %
title = {Industrial-strength
refinement}, %
booktitle = {Proceedings of the Joint Formal Methods
Pacific ’98/International Refinement Workshop ’98 and Conference on Theorem
Proving in Higher-Order Logics, Canberra, Australia, September 1998}, %
series = {Springer Series in Discrete
Mathematics and Theoretical Computer Science}, %
pages = {33--44}, %
year = {1998} %
}%
conference:BoltonDaviesWoodcock99
C. Bolton, J. Davies, J. Woodcock, On the refinement and simulation
of abstract data types. in K. Araki, A. Galloway, K. Taguchi (eds), Proceedings
of the Conference on Integrating Formal Methods, IFM99, Springer.
pp.273–292, 1999.
@inproceedings{%
conference:BoltonDaviesWoodcock99, %
author = {Christie Bolton and
Jim Davies and Jim Woodcock}, %
title = {On the Refinement
and Simulation of Data Types and Processes}, %
booktitle = {IFM}, %
year = {1999}, %
pages = {273-292}, %
crossref =
{proceedings:ArakiGollowayTaguchi99}, %
}%
proceedings:ArakiGollowayTaguchi99
@proceedings{%
proceedings:ArakiGollowayTaguchi99, %
editor = {Keijiro Araki and Andy
Galloway and Kenji Taguchi}, %
title = {Integrated Formal
Methods, Proceedings of the 1st International Conference on Integrated Formal
Methods, IFM 99, York, UK, 28-29 June 1999}, %
booktitle = {IFM}, %
publisher = {Springer}, %
year = {1999}, %
isbm = {1-85233-107-0},
%
}%
conference:CrichtonDaviesWoodcock99
C. Crichton, J. Davies, J. Woodcock, When to trust mobile objects:
access control in the Jini Software System, in D. Firesmith, R. Riehle, G.
Pour, B. Meyer (eds), Proceedings of the IEEE Conference on Technology of Object-Oriented
Languages and Systems, IEEE Computer Society Press, 1999.
@inproceedings{%
conference:CrichtonDaviesWoodcock99, %
author = {Charles Crichton and
Jim Davies and Jim Woodcock}, %
title = {When to Trust Mobile
Objects: Access Control in the Jini(tm) Software System}, %
booktitle = {TOOLS (30)}, %
year = {1999}, %
pages = {116-125}, %
ee = {http://doi.ieeecomputersociety.org/10.1109/TOOLS.1999.787541},
%
crossref = {proceedings:FiresmithRiehlePourMeyer99},
%
}%
proceedings:FiresmithRiehlePourMeyer99
@proceedings{%
proceedings:FiresmithRiehlePourMeyer99, %
editor = {Donald Firesmith and
Richard Riehle and Gilda Pour and Bertrand Meyer}, %
title = {TOOLS 1999: 30th
International Conference on Technology of Object-Oriented Languages and Systems,
Delivering Quality Software - The Way Ahead, 1-5 August 1999, Santa Barbara,
CA, USA}, %
booktitle = {TOOLS (30)}, %
publisher = {IEEE Computer Society}, %
year = {1999}, %
isbm = {0-7695-0278-4},
%
}%
J. Woodcock, Formal refinement: practical industrial experiences,
Proceedings of the 3rd Irish Formal Methods Workshop, IFMW’99, National
University of Ireland, Galway, BCS Electronic Workshops in Computing, 1999.
Keynote speech.
@inproceedings{%
conference:Woodcock99a, %
author = {J. Woodcock}, %
title = {Formal refinement:
practical industrial experiences}, %
booktitle = {Proceedings of the 3rd Irish Formal
Methods Workshop, IFMW’99, National University of Ireland, Galway}, %
series = {BCS Electronic Workshops
in Computing}, %
year = {1999} %
}%
J. Woodcock, A. McEwan, Specifying a Handel-C program in the
Unifying Theory, Proceedings of the Workshop on Parallel Programming, Las
Vegas, Nov 1999.
@inproceedings{%
conference:Woodcock99b, %
author = {J. Woodcock and A. McEwan},
%
title = {Specifying a Handel-C
program in the Unifying Theory}, %
booktitle = {Proceedings of the Workshop on Parallel
Programming, Las Vegas}, %
month = {November}, %
year = {1999} %
}%
J. Woodcock, A. McEwan, An overview of the verification of a
Handel-C program, Proceedings of the International Conference on Parallel and Distributed
Processing Techniques and Applications, IDPT Press, 2000.
@inproceedings{%
conference:WoodcockMcEwan00, %
author = {J. Woodcock and A. McEwan},
%
title = {An overview of
the verification of a Handel-C program}, %
booktitle = {Proceedings of the International Conference
on Parallel and Distributed Processing Techniques and Applications}, %
publisher = {IDPT Press}, %
year = {2000} %
}%
conference:WoodcockCavalcanti01a
J. Woodcock, A. Cavalcanti, A concurrent language for refinement,
in A. Butterfield and C. Pahl (eds), IWFM’01: 5th Irish Workshop in Formal
Methods, Dublin, BCS Electronic Workshops in Computing, 2001.
@inproceedings{%
conference:WoodcockCavalcanti01a, %
author = {Jim Woodcock and Ana
Cavalcanti}, %
title = {A Concurrent Language
for Refinement}, %
booktitle = {IWFM}, %
year = {2001}, %
ee = {http://ewic.bcs.org/conferences/2001/5thformal/papers/paper7.htm},
%
crossref = {proceedings:ButterfieldStrongPahl01},
%
}%
proceedings:ButterfieldStrongPahl01
@proceedings{%
proceedings:ButterfieldStrongPahl01, %
editor = {Andrew Butterfield and
Glenn Strong and Claus Pahl}, %
title = {5th Irish Workshop
on Formal Methods, IWFM 2001, Dublin, Ireland, 16-17 July 2001}, %
booktitle = {IWFM}, %
publisher = {BCS}, %
series = {Workshops in Computing},
%
year = {2001}, %
}%
conference:WoodcockCavalcanti01b
J. Woodcock, A. Cavalcanti, The steam boiler in a unified theory of
Z and CSP, Proceedings of the 8th Asia-Pacific Software Engineering Conference,
Macau, IEEE Computer Society Press, pp.291–298, 2001.
@inproceedings{%
conference:WoodcockCavalcanti01b, %
author = {Jim Woodcock and Ana
Cavalcanti}, %
title = {The Steam
Boiler in a Unified Theory of Z and CSP}, %
booktitle = {APSEC}, %
year = {2001}, %
pages = {291-298}, %
ee = {http://csdl.computer.org/comp/proceedings/apsec/2001/1408/00/14080291abs.htm},
%
crossref = {proceedings:APSEC01}, %
}%
@proceedings{%
proceedings:APSEC01, %
title = {8th Asia-Pacific
Software Engineering Conference (APSEC 2001), 4-7 December 2001, Macau, China},
%
booktitle = {APSEC}, %
organization = {IEEE Computer Society}, %
year = {2001}, %
isbm = {0-7695-1408-1},
%
}%
conference:ButterfieldWoodcock02a
A. Butterfield, J. Woodcock, Semantics of prialt in Handel-C, in J.
Pascoe, P. Welch, R. Loader, V. Sunderam (eds), Communicating Process
Architectures 2002, IOS Press, pp.1–16, 2002.
@inproceedings{%
conference:ButterfieldWoodcock02a, %
author = {A. Butterfield and J.
Woodcock}, %
title = {Semantics of prialt
in Handel-C}, %
editor = {J. Pascoe and P. Welch
and R. Loader and V. Sunderam}, %
booktitle = {Communicating Process Architectures
2002}, %
publisher = {IOS Press}, %
pages = {1--16}, %
year = {2002} %
}%
conference:ButterfieldWoodcock02b
A. Butterfield, J. Woodcock, Semantic domains for Handel-C, in 2nd
Irish Conference on the Mathematical Foundations of Computer Science and
Information Technology, Electronic Notes in Theoretical Computer Science 74:1–20
2002.
@article{%
conference:ButterfieldWoodcock02b, %
author = {Andrew Butterfield and
Jim Woodcock}, %
title = {Semantic domains
for Handel-C}, %
journal = {Electr. Notes Theor. Comput.
Sci.}, %
volume = {74}, %
year = {2002}, %
ee = {http://www1.elsevier.com/gej-ng/31/29/23/143/23/show/Products/notes/index.htt\#002},
%
}%
conference:CavalcantiWoodcock02
A. Cavalcanti, J. Woodcock, A weakest precondition semantics for
Circus, in J. Pascoe, P. Welch, R. Loader, V. Sunderam (eds), Communicating
Process Architectures 2002, IOS Press, pp.147–166. 2002.
@inproceedings{%
conference:CavalcantiWoodcock02, %
author = {A. Cavalcanti and J.
Woodcock}, %
title = {A weakest precondition
semantics for Circus}, %
editor = {J. Pascoe and P. Welch
and R. Loader and V. Sunderam}, %
booktitle = {Communicating Process Architectures
2002}, %
publisher = {IOS Press}, %
pages = {147--166}, %
year = {2002} %
}%
conference:CavalcantiSampaioWoodcock02
A. Cavalcanti, A. Sampaio, J. Woodcock, Refinement of actions in
Circus, Proceedings of REFINE’ 2002, Electronic Notes in Theoretical Computer Science
70(3) 2002. Keynote speech.
@article{%
CavalcantiSampaioWoodcock02, %
author = {Ana Cavalcanti and Augusto
Sampaio and Jim Woodcock}, %
title = {Refinement of actions
in Circus}, %
journal = {Electr. Notes Theor. Comput.
Sci.}, %
volume = {70}, %
number = {3}, %
year = {2002}, %
ee = {http://www.elsevier.com/gej-ng/31/29/23/125/48/show/Products/notes/index.htt\#012},
%
}%
conference:SampaioWoodcockCavalcanti02
A. Sampaio, J. Woodcock, A. Cavalcanti, Refinement in Circus, L.
Eriksson and P. Lindsay (eds), FME 2002: Formal Methods—Getting IT Right, LNCS
2391:451–470, Springer, 2002.
@inproceedings{%
conference:SampaioWoodcockCavalcanti02, %
author = {Augusto Sampaio and
Jim Woodcock and Ana Cavalcanti}, %
title = {Refinement in Circus},
%
booktitle = {FME}, %
year = {2002}, %
pages = {451-470}, %
ee = {http://link.springer.de/link/service/series/0558/bibs/2391/23910451.htm},
%
crossref = {proceedings:ErikssonLindsay02},
%
}%
@proceedings{%
proceedings:ErikssonLindsay02, %
editor = {Lars-Henrik Eriksson
and Peter A. Lindsay}, %
title = {FME 2002: Formal
Methods - Getting IT Right, International Symposium of Formal Methods Europe,
Copenhagen, Denmark, July 22-24, 2002, Proceedings}, %
booktitle = {FME}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {2391}, %
year = {2002}, %
isbm = {3-540-43928-5},
%
}%
J. Woodcock, A. Hughes, Unifying theories of parallel programming, 4th
International Conference on Formal Engineering Methods, ICFEM 2002,
Shanghai, China, Oct 21–25, 2002, LNCS 2495:24–37 2002.
Keynote speech.
@inproceedings{%
conference:WoodcockHughes02, %
author = {Jim Woodcock and Arthur
P. Hughes}, %
title = {Unifying Theories
of Parallel Programming}, %
booktitle = {ICFEM}, %
year = {2002}, %
pages = {24-37}, %
ee = {http://link.springer.de/link/service/series/0558/bibs/2495/24950024.htm},
%
crossref = {proceedings:GeorgeMiao02}, %
}%
@proceedings{%
proceedings:GeorgeMiao02, %
editor = {Chris George and Huaikou
Miao}, %
title = {Formal Methods
and Software Engineering, 4th International Conference on Formal Engineering Methods,
ICFEM 2002 Shanghai, China, October 21-25, 2002, Proceedings}, %
booktitle = {ICFEM}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {2495}, %
year = {2002}, %
isbm = {3-540-00029-1},
%
}%
conference:WoodcockCavalcanti02
J. Woodcock, A. Cavalcanti, The semantics of Circus—a concurrent
language for refinement, Proceedings of ZB 2002—The 2nd International Z and B
Conference, Grenoble, LNCS. 2272:184–203, Springer, 2002.
@inproceedings{%
conference:WoodcockCavalcanti02, %
author = {Jim Woodcock and Ana
Cavalcanti}, %
title = {The Semantics of
Circus}, %
booktitle = {ZB}, %
year = {2002}, %
pages = {184-203}, %
ee = {http://link.springer.de/link/service/series/0558/bibs/2272/22720184.htm},
%
crossref =
{conference:BertBowenHensonRobinson02}, %
}%
conference:BertBowenHensonRobinson02
@proceedings{%
conference:BertBowenHensonRobinson02, %
editor = {Didier Bert and Jonathan
P. Bowen and Martin C. Henson and Ken Robinson}, %
title = {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}, %
booktitle = {ZB}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {2272}, %
year = {2002}, %
isbm = {3-540-43166-7},
%
}%
J. Woodcock, A. McEwan, Verifying the properties of a railway
signalling device, Proceedings of the International Conference on Integrated Design and
Process Technology, Pasadena, IDPT Press, Jun 2002. Rudolph Christian Karl Diesel
best paper award.
@proceedings{%
conference:WoodcockMcEwan02, %
author = {J. Woodcock and A. McEwan},
%
title = {Verifying the properties
of a railway signalling device}, %
booktitle = {Proceedings of the International Conference
on Integrated Design and Process Technology, Pasadena}, %
organization = {IDPT Press}, %
month = {June}, %
year = {2002}, %
note = {Rudolph Christian
Karl Diesel best paper award} %
}%
conference:AtiyaKingWoodcock03
D.-A. Atiya, S. King, J. Woodcock, A Circus semantics for Ravenscar
protected objects, FM 2003: 12th International FME Symposium, Pisa,
LNCS 2805:617–635 2003.
@inproceedings{%
conference:AtiyaKingWoodcock03, %
author = {Diyaa-Addein Atiya and
Steve King and Jim Woodcock}, %
title = {A Circus Semantics
for Ravenscar Protected Objects}, %
booktitle = {FME}, %
year = {2003}, %
pages = {617-635}, %
ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume
=2805{\&}spage=617}, %
crossref = {conference:ArakiGnesiMandrioli03},
%
}%
conference:ArakiGnesiMandrioli03
@proceedings{%
conference:ArakiGnesiMandrioli03, %
editor = {Keijiro Araki and Stefania
Gnesi and Dino Mandrioli}, %
title = {FME 2003: Formal
Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September
8-14, 2003, Proceedings}, %
booktitle = {FME}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {2805}, %
year = {2003}, %
isbm = {3-540-40828-2},
%
}%
conference:ButterfieldWoodcock03
A. Butterfield, J. Woodcock, An operational semantics for Handel-C,
FMICS workshop on Formal Methods for Industrial Critical Systems,
Electronic Notes in Theoretical Computer Science 80 2003.
@article{%
conference:ButterfieldWoodcock03, %
author = {Andrew Butterfield and
Jim Woodcock}, %
title = {An Operational
Semantics for Handel-C}, %
journal = {Electr. Notes Theor. Comput.
Sci.}, %
volume = {80}, %
year = {2003}, %
ee = {http://www1.elsevier.com/gej-ng/31/29/23/137/23/show/Products/notes/index.htt\#017},
%
}%
conference:CavalcantiSampaioWoodcock03
A. Cavalcanti, A. Sampaio, J. Woodcock, A unified language of
classes and processes, St.Eve: State-Oriented vs Event-Oriented Thinking in Requirements Analysis,
Formal Specification, and Software Engineering, Satellite Workshop at
FM’03, 2003.
@inproceedings{%
conference:CavalcantiSampaioWoodcock03, %
author = {A. Cavalcanti and A.
Sampaio and J. Woodcock}, %
title = {A unified language
of classes and processes}, %
booktitle = {St.Eve: State-Oriented vs Event-Oriented
Thinking in Requirements Analysis, Formal Specification, and Software
Engineering, Satellite Workshop at FM’03}, %
year = {2003} %
}%
A. McEwan, J. Woodcock, A refinement-based approach to calculating
a fault-tolerant railway signal device, IFIP Congress Topical Sessions 621–628
2004.
@inproceedings{%
conference:McEwanWoodcock04, %
author = {Alistair A. McEwan and
J. C. P. Woodcock}, %
title = {A refinement based
approach to calculating a fault tolerant railway signal device}, %
booktitle = {IFIP Congress Topical Sessions}, %
year = {2004}, %
pages = {621-628}, %
crossref = {proceedings:Jacquart04} %
}%
@proceedings{%
proceedings:Jacquart04, %
editor = {Ren{\'e} Jacquart},
%
title = {Building the Information
Society, IFIP 18th World Computer Congress, Topical Sessions, 22-27 August
2004, Toulouse, France}, %
booktitle = {IFIP Congress Topical Sessions}, %
publisher = {Kluwer}, %
year = {2004}, %
isbm = {1-4020-8156-1},
%
}%
conference:OliveiraCavalcantiWoodcock04
M. Oliveira, A. Cavalcanti, J. Woodcock, Refining industrial-scale
systems in Circus, in I. East, J. Martin, P. Welch, D. Duce, and M. Green
(eds), Communicating Process Architectures, Concurrent Systems Engineering
Series 62:281–309, IOS Press, 2004.
@inproceedings{%
conference:OliveiraCavalcantiWoodcock04, %
author = {M. Oliveira and A. Cavalcanti
and J. Woodcock}, %
title = {Refining industrial-scale
systems in Circus}, %
editor = {I. East and J. Martin
and P. Welch and D. Duce and M. Green}, %
booktitle = {Communicating Process Architectures},
%
series = {Concurrent Systems Engineering
Series}, %
volume = {62}, %
pages = {281--309}, %
publisher = {IOS Press}, %
year = {2004} %
}%
X. Tang, J. Woodcock, Towards mobile processes in unifying
theories, in J. R. Cuellar and Z. Liu (eds), 2nd IEEE International Conference
on Software Engineering and Formal Methods, IEEE Computer Society Press,
pp.310–319, Sep 2004.
@inproceedings{%
conference:TangWoodcock04a, %
author = {Xinbei Tang and Jim
Woodcock}, %
title = {Towards Mobile
Processes in Unifying Theories}, %
booktitle = {SEFM: 2nd International Conference
on Software Engineering and Formal Methods (SEFM 2004), 28-30 September 2004, Beijing,
China}, %
year = {2004}, %
pages = {44-53}, %
publisher = {IEEE Computer Society}, %
ee = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2004.49}
%
}%
X. Tang, J. Woodcock, Travelling processes, Mathematics of Program
Construction, LNCS 3125 381–399 2004.
@inproceedings{%
conference:TangWoodcock04b, %
author = {Xinbei Tang and Jim
Woodcock}, %
title = {Travelling Processes},
%
booktitle = {MPC}, %
year = {2004}, %
pages = {381-399}, %
ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume
=3125{\&}spage=381}, %
crossref = {proceedings:KozenShankland04}
%
}%
@proceedings{%
proceedings:KozenShankland04, %
editor = {Dexter Kozen and Carron
Shankland}, %
title = {Mathematics of
Program Construction, 7th International Conference, MPC 2004, Stirling, Scotland,
UK, July 12-14, 2004, Proceedings}, %
booktitle = {MPC}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {3125}, %
year = {2004}, %
isbm = {3-540-22380-0},
%
}%
J. Woodcock, Using Circus for safety-critical applications, WMF2003:
6th Brazilian Workshop on Formal Methods, Campina Grande, Brazil, Electronic
Notes in Theoretical Computer Science 95:3–22 2004. Keynote speech.
The Formal Methods Europe Lecture.
@article{%
conference:Woodcock04a, %
author = {Jim Woodcock}, %
title = {Using Circus for
Safety-critical Applications}, %
journal = {Electr. Notes Theor.
Comput. Sci.}, %
volume = {95}, %
year = {2004}, %
pages = {3-22}, %
ee =
{http://dx.doi.org/10.1016/j.entcs.2004.04.003}, %
}%
conference:WoodcockCavalcanti04
J. Woodcock, A. Cavalcanti, A tutorial introduction to designs in
Unifying Theories of Programming, in E. A. Boiten, J. Derrick, G. Smith (eds),
IFM 2004: Integrated Formal Methods, LNCS 2999:40–66, Springer, 2004. Invited
lectures.
@inproceedings{%
conference:WoodcockCavalcanti04, %
author = {Jim Woodcock and Ana
Cavalcanti}, %
title = {A Tutorial Introduction
to Designs in Unifying Theories of Programming}, %
booktitle = {IFM}, %
year = {2004}, %
pages = {40-66}, %
ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume
=2999{\&}spage=40}, %
crossref = {proceedings:BoitenDerrickSmith04},
%
}%
proceedings:BoitenDerrickSmith04
@proceedings{%
proceedings:BoitenDerrickSmith04, %
editor = {Eerke A. Boiten and
John Derrick and Graeme Smith}, %
title = {Integrated Formal
Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 4-7,
2004, Proceedings}, %
booktitle = {IFM}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {2999}, %
year = {2004}, %
isbm = {3-540-21377-5},
%
}%
conference:AtiyaKingWoodcock05
D.-A. Atiya, S. King, J. Woodcock, Simpler reasoning about system
properties: a proof-by-refinement technique, in Proceedings of the REFINE 2005
Workshop (REFINE 2005), Electronic Notes in Theoretical Computer Science 137(2):5–22
2005.
@article{%
conference:AtiyaKingWoodcock05, %
author = {Diyaa-Addein Atiya and
Steve King and Jim Woodcock}, %
title = {Simpler Reasoning
About System Properties: a Proof-by-Refinement Technique}, %
journal = {Electr. Notes Theor. Comput.
Sci.}, %
volume = {137}, %
number = {2}, %
year = {2005}, %
pages = {5-22}, %
ee = {http://dx.doi.org/10.1016/j.entcs.2005.04.022},
%
}%
conference:CavalcantiWoodcock05
A. Cavalcanti, J. Woodcock, Angelic nondeterminism and Unifying
Theories of Programming, in J. Derrick and E. Boiten (eds), REFINE 2005, Electronic
Notes in Theoretical Computer Science 137(2):45–66 2005.
@article{%
conference:CavalcantiWoodcock05, %
author = {Ana Cavalcanti and Jim
Woodcock}, %
title = {Angelic Nondeterminism
and Unifying Theories of Programming}, %
journal = {Electr. Notes Theor. Comput.
Sci.}, %
volume = {137}, %
number = {2}, %
year = {2005}, %
pages = {45-66}, %
ee = {http://dx.doi.org/10.1016/j.entcs.2005.04.024},
%
}%
conference:WoodcockCavalcantiFreitas05
J. Woodcock, A. Cavalcanti, L. Freitas, 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, LNCS
3582:237–252 Springer, 2005.
@inproceedings{%
conference:WoodcockCavalcantiFreitas05, %
author = {Jim Woodcock and Ana
Cavalcanti and Leonardo Freitas}, %
title = {Operational Semantics
for Model Checking Circus}, %
booktitle = {FM}, %
year = {2005}, %
pages = {237-252}, %
ee = {http://dx.doi.org/10.1007/11526841\_17},
%
crossref = {conference:FitzgeraldHayesTarlecki05},
%
}%
conference:FitzgeraldHayesTarlecki05
@proceedings{%
conference:FitzgeraldHayesTarlecki05, %
editor = {John Fitzgerald and
Ian J. Hayes and Andrzej Tarlecki}, %
title = {FM 2005: Formal
Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July
18-22, 2005, Proceedings}, %
booktitle = {FM}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {3582}, %
year = {2005}, %
isbm = {3-540-27882-6},
%
}%
conference:ButterfieldWoodcock06
A. Butterfield, J. Woodcock, A “hardware compiler” semantics for
Handel-C, in Proceedings of the 3rd Irish Conference on the Mathematical Foundations
of Computer Science and Information Technology (MFCSIT 2004) Electronic Notes
in Theoretical Computer Science 161:73–90 2006.
@article{%
conference:ButterfieldWoodcock06, %
author = {Andrew Butterfield and
Jim Woodcock}, %
title = {A "Hardware
Compiler" Semantics for Handel-C}, %
journal = {Electr. Notes Theor. Comput.
Sci.}, %
volume = {161}, %
year = {2006}, %
pages = {73-90}, %
ee = {http://dx.doi.org/10.1016/j.entcs.2006.04.026},
%
}%
conference:CavalcantiHarwoodWoodcock06
A. Cavalcanti, W. Harwood, J. Woodcock, Pointers and records in the
Unifying Theories of Programming, in S. Dunne and B. Stoddart (eds), UTP’06: International
Symposium on Unifying Theories of Programming, Walworth Castle, LNCS
4010:200–216, Springer, 2006.
@inproceedings{%
conference:CavalcantiHarwoodWoodcock06, %
author = {Ana Cavalcanti and Will
Harwood and Jim Woodcock}, %
title = {Pointers and Records
in the Unifying Theories of Programming}, %
booktitle = {UTP}, %
year = {2006}, %
pages = {200-216}, %
ee = {http://dx.doi.org/10.1007/11768173\_12},
%
crossref = {proceedings:DunneStoddart06},
%
}%
@proceedings{%
proceedings:DunneStoddart06, %
editor = {Steve Dunne and Bill
Stoddart}, %
title = {Unifying Theories
of Programming, First International Symposium, UTP 2006, Walworth Castle,
County Durham, UK, February 5-7, 2006, Revised Selected Papers}, %
booktitle = {UTP}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {4010}, %
year = {2006}, %
isbm = {3-540-34750-X},
%
}%
conference:FreitasCavalcantiWoodcock06
L. Freitas, A. Cavalcanti, J. Woodcock, Taking our own medicine:
Applying the refinement calculus to state-rich refinement model checking, in Z.
Liu and J. He (eds), Formal Methods and Software Engineering, 8th International Conference
on Formal Engineering Methods, ICFEM 2006, Guiyang, China, LNCS
4260:697–716, Springer, 2006.
@inproceedings{%
conference:FreitasCavalcantiWoodcock06, %
author = {Leo Freitas and Ana
Cavalcanti and Jim Woodcock}, %
title = {Taking Our Own
Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking},
%
booktitle = {ICFEM}, %
year = {2006}, %
pages = {697-716}, %
ee = {http://dx.doi.org/10.1007/11901433\_38},
%
crossref = {proceedings:LiuHe06}, %
}%
@proceedings{%
proceedings:LiuHe06, %
editor = {Zhiming Liu and Jifeng
He}, %
title = {Formal Methods
and Software Engineering, 8th International Conference on Formal Engineering Methods,
ICFEM 2006, Macao, China, November 1-3, 2006, Proceedings}, %
booktitle = {ICFEM}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {4260}, %
year = {2006}, %
isbm = {3-540-47460-9},
%
}%
G. Nuka, J. Woodcock, Mechanising a unifying theory, in S. Dunne
and B. Stoddart (eds), UTP’06: International Symposium on Unifying Theories of
Programming, Walworth Castle, LNCS 4010:217–235, Springer, 2006.
@inproceedings{%
conference:NukaWoodcock06, %
author = {Gift Nuka and Jim Woodcock},
%
title = {Mechanising a Unifying
Theory}, %
booktitle = {UTP}, %
year = {2006}, %
pages = {217-235}, %
ee = {http://dx.doi.org/10.1007/11768173\_13},
%
crossref = {proceedings:DunneStoddart06},
%
}%
conference:OliveiraCavalcantiWoodcock06
M. Oliveira, A. Cavalcanti, J. Woodcock, Unifying theories in
ProofPower-Z, in S. Dunne and B. Stoddart (eds), UTP’06: International
Symposium on Unifying Theories of Programming, Walworth Castle, LNCS
4010:123–140, Springer 2006.
@inproceedings{%
conference:OliveiraCavalcantiWoodcock06, %
author = {Marcel Oliveira and
Ana Cavalcanti and Jim Woodcock}, %
title = {Unifying Theories
in ProofPower-Z}, %
booktitle = {UTP}, %
year = {2006}, %
pages = {123-140}, %
ee = {http://dx.doi.org/10.1007/11768173\_8},
%
crossref = {proceedings:DunneStoddart06},
%
}%
conference:SchneiderTreharneCavalcantiWoodcock06
S. Schneider, A. Cavalcanti, H. Treharne, J. Woodcock, A layered
behavioural model of platelets, in Proceedings 11th International Conference on
Engineering of Complex Computer Systems, pp.98–106, IEEE Computer Society
Press, 2006.
@inproceedings{%
conference:SchneiderTreharneCavalcantiWoodcock06, %
author = {Steve Schneider and
Helen Treharne and Ana Cavalcanti and Jim Woodcock}, %
title = {A Layered Behavioural
Model of Platelets}, %
booktitle = {ICECCS: 11th International Conference
on Engineering of Complex Computer Systems (ICECCS 2006), 15-17 August 2006,
Stanford, California, USA}, %
year = {2006}, %
pages = {98-106}, %
publisher = {IEEE Computer Society}, %
ee = {http://doi.ieeecomputersociety.org/10.1109/ICECCS.2006.80},
%
}%
J. Woodcock, First steps in the Verified Software Grand Challenge, 30th
Annual IEEE / NASA Software Engineering Workshop (SEW-30 2006),
203–206, 25–28 Apr 2006, Loyola College Graduate Center, Columbia, IEEE
Computer Society, 2006.
@inproceedings{%
conference:Woodcock06a, %
author = {Jim Woodcock}, %
title = {First Steps in
the Verified Software Grand Challenge}, %
booktitle = {SEW}, %
year = {2006}, %
pages = {203-206}, %
ee = {http://doi.ieeecomputersociety.org/10.1109/SEW.2006.17},
%
crossref = {proceedings:SEW06}, %
}%
@proceedings{%
proceedings:SEW06, %
title = {30th Annual IEEE
/ NASA Software Engineering Workshop (SEW-30 2006), 25-28 April 2006, Loyola
College Graduate Center, Columbia, MD, USA}, %
booktitle = {SEW}, %
publisher = {IEEE Computer Society}, %
year = {2006}, %
}%
J. Woodcock, Verified Software Grand Challenge, in J. Misra, T.
Nipkow, E. Sekerinski (eds), FM 2006: Formal Methods, 14th International
Symposium on Formal Methods, Hamilton, Canada, Aug 21-27, 2006, Proceedings,
LNCS 4085:617–617, Springer, 2006.
@inproceedings{%
conference:Woodcock06b, %
author = {Jim Woodcock}, %
title = {Verified Software
Grand Challenge}, %
booktitle = {FM}, %
year = {2006}, %
pages = {617-617}, %
ee = {http://dx.doi.org/10.1007/11813040\_45},
%
crossref = {DBLP:conf/fm/2006}, %
}%
J. Woodcock, An operational semantics in UTP for a language of
reactive designs (abstract), in S. Dunne and B. Stoddart (eds), UTP’06:
International Symposium on Unifying Theories of Programming, Walworth Castle,
LNCS 4010:84–84, Springer 2006.
@inproceedings{%
conference:Woodcock06c, %
author = {Jim Woodcock}, %
title = {An Operational
Semantics in UTP for a Language of Reactive Designs (Abstract)}, %
booktitle = {UTP}, %
year = {2006}, %
pages = {84-84}, %
ee = {http://dx.doi.org/10.1007/11768173\_5},
%
crossref = {proceedings:DunneStoddart06},
%
}%
J. Woodcock, L. Freitas, Z/Eves and the Mondex electronic purse, Theoretical
Aspects of Computing — ICTAC 2006, LNCS 4281:15–34 2006.
@inproceedings{%
conference:WoodcockFreitas06, %
author = {Jim Woodcock and Leo
Freitas}, %
title = {Z/Eves and the
Mondex Electronic Purse}, %
booktitle = {ICTAC}, %
year = {2006}, %
pages = {15-34}, %
ee = {http://dx.doi.org/10.1007/11921240\_2},
%
crossref = {proceedings:BarkaouiCavalcantiCerone06},
%
}%
proceedings:BarkaouiCavalcantiCerone06
@proceedings{%
proceedings:BarkaouiCavalcantiCerone06, %
editor = {Kamel Barkaoui and Ana
Cavalcanti and Antonio Cerone}, %
title = {Theoretical Aspects
of Computing - ICTAC 2006, Third International Colloquium, Tunis, Tunisia,
November 20-24, 2006, Proceedings}, %
booktitle = {ICTAC}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {4281}, %
year = {2006}, %
isbm = {3-540-48815-4},
%
}%
conference:AydalPaigeWoodcock07
E. Aydal, R. Paige, J. Woodcock, Evaluation of OCL for large-scale
modelling: a different view of the Mondex smart card application, Ocl4All:
Modelling Systems with OCL, MODELS’07, Nashville, Sep 2007.
@inproceedings{%
conference:AydalPaigeWoodcock07, %
author = {E. Aydal and R. Paige
and J. Woodcock}, %
title = {Evaluation of OCL
for large-scale modelling: a different view of the Mondex smart card application},
%
booktitle = {Ocl4All: Modelling Systems with OCL,
MODELS’07, Nashville}, %
month = {Septmeber}, %
year = {2007} %
}%
conference:AydalWoodcockCavalcanti07
E. Aydal, J. Woodcock, A. Cavalcanti, Goal-oriented automatic
test-case generators for MC/DC compliancy, ICSOFT’07, Barcelona, Spain, Jul
2007.
@inproceedings{%
conference:AydalWoodcockCavalcanti07, %
author = {E. Aydal and J. Woodcock
and A. Cavalcanti}, %
title = {Goal-oriented automatic
test-case generators for MC/DC compliancy}, %
booktitle = {ICSOFT’07, Barcelona, Spain}, %
month = {July}, %
year = {2007} %
}%
conference:ButterfieldSherifWoodcock07
A. Butterfield, A. Sherif, J. Woodcock, Slotted Circus. Integrated
Formal Methods: 6th International Conference, IFM 2007,
Oxford, 2–5 Jul 2007, Proceedings, LNCS 4591 2007.
@inproceedings{%
proceedings:ButterfieldSherifWoodcock07, %
author = {Andrew Butterfield and
Adnan Sherif and Jim Woodcock}, %
title = {Slotted-Circus},
%
booktitle = {IFM}, %
year = {2007}, %
pages = {75-97}, %
ee = {http://dx.doi.org/10.1007/978-3-540-73210-5\_5},
%
crossref = {proceedings:DaviesGibbons07},
%
}%
@proceedings{%
proceedings:DaviesGibbons07, %
editor = {Jim Davies and Jeremy
Gibbons}, %
title = {Integrated Formal
Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007,
Proceedings}, %
booktitle = {IFM}, %
publisher = {Springer}, %
series = {Lecture Notes in Computer
Science}, %
volume = {4591}, %
year = {2007}, %
isbm =
{978-3-540-73209-9}, %
}%
conference:ButterfieldWoodcock07
A. Butterfield, J. Woodcock, Formalising flash memory: first steps,
ICECCS: 12th International Conference on Engineering of Complex Computer
Systems 2006, Auckland, New Zealand, 2007.
@inproceedings{%
conference:ButterfieldWoodcock07, %
author = {Andrew Butterfield and
Jim Woodcock}, %
title = {Formalising Flash
Memory: First Steps}, %
booktitle = {ICECCS}, %
year = {2007}, %
pages = {251-260}, %
ee = {http://doi.ieeecomputersociety.org/10.1109/ICECCS.2007.23},
%
crossref = {proceedings:ICECCS07}, %
}%
@proceedings{%
proceedings:ICECCS07, %
title = {12th International
Conference on Engineering of Complex Computer Systems (ICECCS 2007), 10-14 July
2007, Auckland, New Zealand}, %
booktitle = {ICECCS}, %
publisher = {IEEE Computer Society}, %
year = {2007}, %
isbm = {978-0-7695-2895-3},
%
}%
conference:FreitasFuWoodcock07
L. Freitas, Z. Fu, J. Woodcock, POSIX file store in Z/Eves: An
experiment in the Verified Software Repository, ICECCS: 12th International
Conference on Engineering of Complex Computer Systems 2006,
Auckland, New Zealand, 2007.
@inproceedings{%
conference:FreitasFuWoodcock07, %
author = {Leo Freitas and Zheng
Fu and Jim Woodcock}, %
title = {POSIX file store
in Z/Eves: an experiment in the verified software repository}, %
booktitle = {ICECCS}, %
year = {2007}, %
pages = {3-14}, %
ee = {http://doi.ieeecomputersociety.org/10.1109/ICECCS.2007.36},
%
crossref = {proceedings:ICECCS2007} %
}%
@proceedings{%
proceedings:ICECCS2007, %
title = {12th International
Conference on Engineering of Complex Computer Systems (ICECCS 2007), 10-14 July
2007, Auckland, New Zealand}, %
booktitle = {ICECCS}, %
publisher = {IEEE Computer Society}, %
year = {2007}, %
isbm = {978-0-7695-2895-3},
%
}%
conference:FreitasMokosWoodcock07
L. Freitas, K. Mokos, J. Woodcock, Verifying the CICS File Control
API with Z/Eves: An experiment in the Verified Software Repository, ICECCS:
12th International Conference on Engineering of Complex Computer Systems 2006,
Auckland, New Zealand, 2007.
@inproceedings{%
FreitasMokosWoodcock07, %
author = {Leo Freitas and Konstantinos
Mokos and Jim Woodcock}, %
title = {Verifying the CICS
File Control API with Z/Eves: An Experiment in the Verified Software Repository},
%
booktitle = {ICECCS}, %
year = {2007}, %
pages = {290-298}, %
ee = {http://doi.ieeecomputersociety.org/10.1109/ICECCS.2007.45},
%
crossref = {proceedings:ICECCS2007}, %
}%
L. Freitas, J. Woodcock, FDR Explorer, Electronic Notes in
Theoretical Computer Science 187:19–34 2007.
@article{%
journal:FreitasWoodcock07, %
author = {Leo Freitas and Jim
Woodcock}, %
title = {FDR Explorer},
%
journal = {Electr. Notes Theor. Comput.
Sci.}, %
volume = {187}, %
year = {2007}, %
pages = {19-34}, %
ee = {http://dx.doi.org/10.1016/j.entcs.2006.08.042},
%
}%
conference:OliveiraCavalcantiWoodcock07
M. Oliveira, A. Cavalcanti, J. Woodcock, A denotational semantics
for Circus, in B. Aichernig and J. Derrick (eds), REFINE’2006, Electronic Notes
in Theoretical Computer Science 187:107–123 2007 .
@article{%
conference:OliveiraCavalcantiWoodcock07, %
author = {Marcel Oliveira and
Ana Cavalcanti and Jim Woodcock}, %
title = {A Denotational
Semantics for Circus}, %
journal = {Electr. Notes Theor. Comput.
Sci.}, %
volume = {187}, %
year = {2007}, %
pages = {107-123}, %
ee = {http://dx.doi.org/10.1016/j.entcs.2006.08.047},
%
}%
M. Oliveira, J. Woodcock, Automatic generation of verified
concurrent hardware, International Conference on Formal Engineering Methods, ICFEM 2007, LNCS,
Springer, 2007.@inproceedings{%
conference:Woodcock07, %
author = {M. Oliveira and J. Woodcock},
%
title = {Automatic generation
of verified concurrent hardware}, %
booktitle = {International Conference on Formal
Engineering Methods, ICFEM 2007}, %
series = {LNCS}, %
publisher = {Springer}, %
year = {2007} %
}%
J. Perna, J. Woodcock, A denotational semantics in HOL for Handel-C
hardware compilation, International Conference on Formal Engineering Methods, ICFEM 2007, LNCS,
Springer, 2007.
@inproceedings{%
conference:PernaWoodcock07, %
author = {J. Perna and J. Woodcock},
%
title = {A denotational
semantics in HOL for Handel-C hardware compilation}, %
booktitle = {International Conference on Formal
Engineering Methods, ICFEM 2007}, %
series = {LNCS}, %
publisher = {Springer}, %
year = {2007} %
}%
J. Woodcock, E6: Use of formality, Video tape G3A tape No. 68,
Government Communications Headquarters, Communications-Electronics Security
Group, Unclassified document, Oct 1997.
@misc{%
misc:Woodcock97, %
author = {J. Woodcock}, %
title = {E6: Use of formality,
Video tape G3A tape No. 68}, %
organization = {Government Communications Headquarters, Communications-Electronics
Security Group}, %
hopublished = {Unclassified document}, %
month = {October}, %
year = {1997} %
}%
J. Wing, J. Woodcock, J. Davies, World Congress on Formal Methods
FM99: Proceedings, Tutorials, and additional materials, CD,
Springer, Sep 1999.
@misc{%
misc:WingWoodcockDavies99, %
author = {J. Wing and J. Woodcock
and J. Davies}, %
title = {World Congress
on Formal Methods FM99: Proceedings, Tutorials, and additional materials}, %
howpublished = {CD}, %
publisher = {Springer}, %
month = {September}, %
year = {1999} %
}%
J. Woodcock, S. Stepney, Software Engineering Research at Oxford,
The Oxford Story, Video recorded interviews, 1999.
@misc{%
misc:WoodcockStepney99, %
author = {J. Woodcock and S. Stepney},
%
title = {Software Engineering
Research at Oxford, The Oxford Story}, %
howpublished = {Video recorded interviews}, %
year = {1999} %
}%
misc:DerrickBoitenWoodcockVonWright02
J. Derrick, E. A. Boiten, J. Woodcock, J. von Wright, Preface, Electronic
Notes in Theoretical Computer Science 70(3) 2002.
@article{%
misc:DerrickBoitenWoodcockVonWright02, %
author = {J. Derrick and E. A.
Boiten and J. Woodcock and J. von Wright}, %
title = {Preface}, %
journal = {Electronic Notes in Theoretical
Computer Science}, %
volume = {70}, %
number = {3}, %
year = {2002} %
}%
J. Woodcock, Software Engineering Mathematics, Microsoft Reader
eBook (Windows 98+, Tablet PC, Pocket PC 2003), eBookMall, 2007.
@book{%
misc:Woodcock07, %
author = {J. Woodcock}, %
title = {Software Engineering
Mathematics, Microsoft Reader eBook (Windows 98+, Tablet PC, Pocket PC 2003)},
%
publisher = {eBookMall}, %
year = {2007} %
}%
Selected Reports
D. Pitt, J. Woodcock, The Importance of Time in the Specification
of OSI Protocols, Report NPLDITC-78/86, National Physical Laboratory,
Teddington, Nov 1986.
@techreport{%
report:PittWoodcock86, %
author = {D. Pitt and J. Woodcock},
%
title = {The Importance
of Time in the Specification of OSI Protocols}, %
type = {Report}, %
number = {NPLDITC-78/86}, %
institution = {National Physical Laboratory, Teddington}, %
month = {November}, %
year = {1986} %
}%
J. Woodcock, Teaching how to use mathematics for large-scale
software development. Bulletin of BCS-FACS, Jul 1988.
@article{%
report:Woodcock88, %
author = {J. Woodcock}, %
title = {Teaching how to
use mathematics for large-scale software development}, %
journal = {Bulletin of BCS-FACS}, %
month = {July}, %
year = {1988} %
}%
J. Woodcock, Case Studies in Proof in Z, DTI IED Zip Project
Deliverable, 1992.
@techreport{%
report:Woodcock92a, %
author = {J. Woodcock}, %
title = {Case Studies in
Proof in Z}, %
type = {DTI IED Zip
Project Deliverable}, %
year = {1992} %
}%
J. Woodcock, Standards for the use of Z, Formal Systems (Europe)
Ltd, Technical Memorandum SRC/ZS/1 version 1.4, Dec 1992.
@techreport{%
report:Woodcock92b, %
author = {J. Woodcock}, %
title = {Standards for the
use of Z}, %
organization = {Formal Systems (Europe) Ltd}, %
type = {Technical
Memorandum}, %
number = {SRC/ZS/1 version 1.4},
%
month = {December}, %
year = {1992} %
}%
J.
Woodcock, Interim Defence Standard 00–56 Safety Analysis Elements: revised
formal specification, Formal Systems (Europe) Ltd, Technical Memorandum
SRC/RDS-SAE/1 version 1.9, Apr 1993.
@techreport{%
report:Woodcock93, %
author = {J. Woodcock}, %
title = {Interim Defence
Standard 00--56 Safety Analysis Elements: revised formal specification}, %
institution = {Formal Systems (Europe) Ltd}, %
type = {Technical
Memorandum}, %
number = {SRC/RDS-SAE/1 version
1.9}, %
month = {April}, %
year = {1993} %
}%
J. Woodcock, J. Hulance, A Rigorous Development of a Process
Scheduler, Formal Systems (Europe) Ltd, Technical Memorandum CSDL/PS/1, Feb
1994.
@techreport{%
report:WoodcockHulance94, %
author = {J. Woodcock and J. Hulance},
%
title = {A Rigorous Development
of a Process Scheduler}, %
institution = {Formal Systems (Europe) Ltd}, %
type = {Technical
Memorandum}, %
number = {CSDL/PS/1}, %
month = {February}, %
year = {1994} %
}%
ISO Panel, Z Notation: version 1.2. Draft British and International
Standard, available as BSI Panel IST/5/- /19/2 (Z Notation), ISO Panel JTC1/SC22/WG19
(Rapporteur Group for Z), 14 Sep 1995. 210pp.
@techreport{%
report:ISOPanel95, %
author = {ISO Panel}, %
title = {Z Notation: version
1.2. Draft British and International Standard, available as BSI Panel IST/5/-
/19/2 (Z Notation)}, %
institution = {ISO Panel JTC1/SC22/WG19 (Rapporteur Group for
Z)}, %
month = {14 September},
%
year = {1995}, %
size = {210pp.} %
}%
report:CooperStepneyWoodcock02
D. Cooper, S. Stepney, J. Woodcock, Derivation of Z Refinement
Proof Rules: Forwards and Backwards Rules Incorporating Input/Output Refinement,
University of York, Department of Computer Science, YCS-2002-347, 2002.
@techreport{%
report:CooperStepneyWoodcock02, %
author = {D. Cooper and S. Stepney
and J. Woodcock}, %
title = {Derivation of Z
Refinement Proof Rules: Forwards and Backwards Rules Incorporating Input/Output
Refinement}, %
institution = {University of York, Department of Computer Science},
%
number = {YCS-2002-347}, %
year = {2002} %
}%
J. Woodcock, A. Cavalcanti, Circus: a Concurrent Refinement
Language, Technical Report, University of Kent and Federal University of
Pernambuco, 2002.
@techreport{%
report:WoodcockCavalcanti02, %
author = {J. Woodcock and A. Cavalcanti},
%
title = {Circus: a Concurrent
Refinement Language}, %
type = {Technical
Report}, %
institution = {University of Kent and Federal University
of Pernambuco}, %
year = {2002} %
}%
J. Woodcock, A. Hughes, Unifying Theories of Parallel Programming,
Notes for Marktoberdorf Summer School, Technical University of Munich, 2002.
@techreport{%
report:WoodcockHughes02, %
author = {J. Woodcock and A. Hughes},
%
title = {Unifying Theories
of Parallel Programming}, %
type = {Notes for
Marktoberdorf Summer School}, %
institution = {Technical University of Munich}, %
year = {2002} %
}%
D.-A. Atiya, S. King, J. Woodcock, Ravenscar Protected Objects: a
Circus Semantics, Research Report YCS 356(2003), University of York, Dept of
Computer Science, 2003.
@techreport{%
report:AtiyaKingWoodcock03, %
author = {D.-A. Atiya and S. King
and J. Woodcock}, %
title = {Ravenscar Protected
Objects: a Circus Semantics}, %
type = {Research Report},
%
number = {YCS 356(2003)}, %
institution = {University of York, Dept of Computer
Science}, %
year = {2003} %
}%
A. Cavalcanti, J. Woodcock, Angelic Nondeterminism and Unifying
Theories of Programming (Extended Version), Computing Laboratory,
University of Kent, 2004.
@techreport{%
report:CavalcantiWoodcock04, %
author = {A. Cavalcanti and J.
Woodcock}, %
title = {Angelic Nondeterminism
and Unifying Theories of Programming (Extended Version)}, %
institution = {Computing Laboratory, University of Kent}, %
year = {2004} %
}%
Jim Woodcock, 22
November 2007