×

Woodcock, James C. P.

Compute Distance To:
Author ID: woodcock.james-c-p Recent zbMATH articles by "Woodcock, James C. P."
Published as: Woodcock, Jim; Woodcock, J. C. P.; Woodcock, James C. P.; Woodcock, Jim C. P.
External Links: ORCID
all top 5

Co-Authors

4 single-authored
32 Cavalcanti, Ana
11 Foster, Simon
8 Liu, Zhiming
7 Freitas, Leo
5 Davies, Jim
5 Oliveira, Marcel
5 Sampaio, Augusto C. A.
5 Zeyda, Frank
4 Perna, Juan Ignacio
4 Wei, Kun
3 Jones, Cliff B.
3 Ye, Kangfeng
3 Zhu, Huibiao
2 Bandur, Victor
2 Butterfield, Andrew
2 Canham, Samuel
2 Chapman, Rod
2 Dong, JinSong
2 Harwood, Will
2 Hoare, C. A. R. Tony
2 King, Steve F.
2 Mota, Alexandre C.
2 Simpson, Andrew
2 Wellings, Andy
1 Amálio, Nuno
1 Atiya, D.
1 Aydal, Emine Gökçe
1 Barnes, Janet
1 Bicarregui, Juan C.
1 Bird, Richard S.
1 Boiten, Eerke A.
1 Bolton, Christie
1 Brooke, Phillip J.
1 Burns, Alan D.
1 Calinescu, Radu C.
1 Chen, Taolue
1 Chen, Xiaoping
1 Cheng, Shu
1 Cooke, John
1 Déharbe, David
1 Derrick, John
1 D’Souza, Deepak
1 Dunne, Steve E.
1 Fantechi, Alessandro
1 Fu, Zheng
1 Gardiner, Paul H. B.
1 Gaudel, Marie-Claude
1 George, Chris W.
1 Gleirscher, Mario
1 Haxthausen, Anne Elisabeth
1 Huang, Wenling
1 Hughes, Arthur
1 Iyoda, Juliano
1 Kröning, Daniel
1 Larsen, Peter Gorm
1 Loomes, Martin
1 Margaria, Tiziana
1 McEwan, Alistair A.
1 Morgan, C. Carroll
1 Ngondi, Gerard Ekembe
1 Nuka, Gift
1 O’Halloran, Colin
1 Paige, Richard F.
1 Peleska, Jan
1 Proietti, Maurizio
1 Qin, Shengchao
1 Ribeiro, Pedro
1 Roscoe, Andrew William
1 Santen, Thomas
1 Seki, Hirohisa
1 Shankar, Natarajan
1 Struth, Georg
1 Tang, Xinbei
1 Thiele, Bernhard
1 von Wright, Joakim
1 Wang, Ji
1 Wing, Jeannette Marie
1 Wulf, Lasse
1 Zeng, Xia
1 Zhang, Wenhui
1 Zhang, Yichi
1 Zhao, Hengjun

Publications by Year

Citations contained in zbMATH Open

57 Publications have been cited 356 times in 164 Documents Cited by Year
Using Z. Specification, refinement, and proof. Zbl 0855.68060
Woodcock, Jim; Davies, Jim
87
1996
A UTP semantics for Circus. Zbl 1165.68048
Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim
29
2009
A refinement strategy for Circus. Zbl 1093.68555
Cavalcanti, Ana; Sampaio, Augusto; Woodcock, Jim
23
2003
The semantics of Circus. Zbl 1044.68560
Woodcock, Jim; Cavalcanti, Ana
22
2002
A theory of pointers for the UTP. Zbl 1161.68388
Harwood, Will; Cavalcanti, Ana; Woodcock, Jim
13
2008
Unifying theories in ProofPower-Z. Zbl 1186.68090
Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim
11
2006
Isabelle/UTP: a mechanised theory engineering framework. Zbl 1457.68061
Foster, Simon; Zeyda, Frank; Woodcock, Jim
10
2015
ZRC – A refinement calculus for \(Z\). Zbl 0934.68062
Cavalcanti, Ana; Woodcock, Jim
9
1998
A tutorial introduction to designs in unifying theories of programming. Zbl 1196.68031
Woodcock, Jim; Cavalcanti, Ana
9
2004
Angelic nondeterminism in the unifying theories of programming. Zbl 1105.68012
Cavalcanti, Ana; Woodcock, Jim; Dunne, Steve
8
2006
A tactic calculus. — Abridged version. Zbl 0857.68094
Martin, A. P.; Gardiner, P. H. B.; Woodcock, J. C. P.
8
1996
On the refinement and simulation of data types and processes. Zbl 0963.68126
Bolton, Christie; Davies, Jim; Woodcock, Jim
7
1999
ArcAngel: a tactic language for refinement. Zbl 1093.68565
Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim
7
2003
Mechanising a unifying theory. Zbl 1186.68089
Nuka, Gift; Woodcock, Jim
7
2006
Operational semantics for model checking Circus. Zbl 1120.68423
Woodcock, Jim; Cavalcanti, Ana; Freitas, Leonardo
6
2005
Refinement in Circus. Zbl 1064.68539
Sampaio, Augusto; Woodcock, Jim; Cavalcanti, Ana
6
2002
The miracle of reactive programming. Zbl 1286.68096
Woodcock, Jim
6
2010
The safety-critical Java memory model formalised. Zbl 1259.68029
Cavalcanti, Ana; Wellings, Andy; Woodcock, Jim
6
2013
Unifying theories in ProofPower-Z. Zbl 1259.68035
Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim
6
2013
Towards a UTP semantics for Modelica. Zbl 06700457
Foster, Simon; Thiele, Bernhard; Cavalcanti, Ana; Woodcock, Jim
6
2017
Circus Time with reactive designs. Zbl 1452.68057
Wei, Kun; Woodcock, Jim; Cavalcanti, Ana
5
2013
Z/Eves and the mondex electronic purse. Zbl 1168.68544
Woodcock, Jim; Freitas, Leo
5
2006
UTP semantics for Handel-C. Zbl 1286.68035
Perna, Juan Ignacio; Woodcock, Jim
4
2010
Pointers and records in the unifying theories of programming. Zbl 1186.68107
Cavalcanti, Ana; Harwood, Will; Woodcock, Jim
4
2006
Unifying heterogeneous state-spaces with lenses. Zbl 1482.68089
Foster, Simon; Zeyda, Frank; Woodcock, Jim
4
2016
Unifying theories of time with generalised reactive processes. Zbl 1476.68143
Foster, Simon; Cavalcanti, Ana; Woodcock, Jim; Zeyda, Frank
3
2018
Travelling processes. Zbl 1106.68347
Tang, Xinbei; Woodcock, Jim
3
2004
POSIX file store in Z/Eves: An experiment in the verified software repository. Zbl 1162.68388
Freitas, Leo; Woodcock, Jim; Fu, Zheng
3
2009
Angelic nondeterminism and unifying theories of programming. Zbl 1276.68054
Cavalcanti, Ana; Woodcock, Jim
2
2005
Software engineering mathematics. Zbl 0825.68032
Woodcock, Jim; Loomes, Martin
2
1988
The verified software repository: a step towards the verifying compiler. Zbl 1103.68452
Bicarregui, J. C.; Hoare, C. A. R.; Woodcock, J. C. P.
2
2006
The tokeneer experiments. Zbl 1213.68391
Woodcock, Jim; Aydal, Emine Gökçe; Chapman, Rod
2
2010
Unifying theories of parallel programming. Zbl 1015.68819
Woodcock, Jim; Hughes, Arthur
2
2002
A weakest precondition semantics for Z. Zbl 0906.68093
Cavalcanti, Ana; Woodcock, Jim
2
1998
Proving theorems about JML classes. Zbl 1151.68348
Freitas, Leo; Woodcock, Jim
2
2007
Mechanising a formal model of flash memory. Zbl 1162.68387
Butterfield, Andrew; Freitas, Leo; Woodcock, Jim
2
2009
Unifying theories of reactive design contracts. Zbl 1436.68195
Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank
2
2020
Three approaches to timed external choice in UTP. Zbl 1457.68059
Canham, Samuel; Woodcock, Jim
2
2015
Transaction processing primitives and CSP. Zbl 0629.68018
Woodcock, J. C. P.
1
1987
Simpler reasoning about system properties: a proof-by-refinement technique. Zbl 1276.68052
Atiya, D.; King, S.; Woodcock, J. C. P.
1
2005
Safety-critical Java programs from Circus models. Zbl 1285.68037
Cavalcanti, Ana; Zeyda, Frank; Wellings, Andy; Woodcock, Jim; Wei, Kun
1
2013
Mechanised wire-wise verification of Handel-C synthesis. Zbl 1347.68235
Perna, Juan Ignacio; Woodcock, Jim
1
2009
Security management via \(Z\) and CSP. Zbl 0924.68139
Simpson, Andrew; Davies, Jim; Woodcock, Jim
1
1998
An inconsistency in procedures, parameters, and substitution in the refinement calculus. Zbl 0942.68014
Cavalcanti, Ana; Sampaio, Augusto; Woodcock, Jim
1
1999
FM ’99. Formal methods. World congress on Formal methods in the development of computing systems. Toulouse, France, September 20–24, 1999. Proceedings. In 2 vols. Zbl 0929.00076
1
1999
Unifying theories of interrupts. Zbl 1286.68088
McEwan, Alistair A.; Woodcock, Jim
1
2010
REFINE 2002. Proceedings of the BCS FACS refinement workshop (satellite event of FLoC 2002), Copenhagen, Denmark, July 20–21, 2002. Zbl 1270.68022
1
2002
Simulink timed models for program verification. Zbl 1390.68423
Cavalcanti, Ana; Mota, Alexandre; Woodcock, Jim
1
2013
Refinement of actions in Circus. Zbl 1270.68079
Cavalcanti, Ana; Sampaio, Augusto; Woodcock, Jim
1
2002
Semantic domains for Handel-C. Zbl 1270.68151
Butterfield, Andrew; Woodcock, Jim
1
2003
Unifying theories of programming and formal engineering methods. International training school on software engineering, held at ICTAC 2013, Shanghai, China, August 26–30, 2013. Advanced lectures. Zbl 1320.68021
1
2013
Unifying theories of programming in Isabelle. Zbl 1444.68049
Foster, Simon; Woodcock, Jim
1
2013
UTP semantics of reactive processes with continuations. Zbl 06700460
Ngondi, Gerard Ekembe; Woodcock, Jim
1
2017
Calculational verification of reactive programs with reactive relations and Kleene algebra. Zbl 06975211
Foster, Simon; Ye, Kangfeng; Cavalcanti, Ana; Woodcock, Jim
1
2018
Using formal reasoning on a model of tasks for FreeRTOS. Zbl 1328.68044
Cheng, Shu; Woodcock, Jim; D’Souza, Deepak
1
2015
CSP and Kripke structures. Zbl 1471.68135
Cavalcanti, Ana; Huang, Wen-ling; Peleska, Jan; Woodcock, Jim
1
2015
Formal methods: Foundations and applications. 12th Brazilian symposium on formal methods, SBMF 2009, Gramado, Brazil, August 19–21, 2009. Revised selected papers. Zbl 1177.68016
1
2009
Unifying theories of reactive design contracts. Zbl 1436.68195
Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank
2
2020
Unifying theories of time with generalised reactive processes. Zbl 1476.68143
Foster, Simon; Cavalcanti, Ana; Woodcock, Jim; Zeyda, Frank
3
2018
Calculational verification of reactive programs with reactive relations and Kleene algebra. Zbl 06975211
Foster, Simon; Ye, Kangfeng; Cavalcanti, Ana; Woodcock, Jim
1
2018
Towards a UTP semantics for Modelica. Zbl 06700457
Foster, Simon; Thiele, Bernhard; Cavalcanti, Ana; Woodcock, Jim
6
2017
UTP semantics of reactive processes with continuations. Zbl 06700460
Ngondi, Gerard Ekembe; Woodcock, Jim
1
2017
Unifying heterogeneous state-spaces with lenses. Zbl 1482.68089
Foster, Simon; Zeyda, Frank; Woodcock, Jim
4
2016
Isabelle/UTP: a mechanised theory engineering framework. Zbl 1457.68061
Foster, Simon; Zeyda, Frank; Woodcock, Jim
10
2015
Three approaches to timed external choice in UTP. Zbl 1457.68059
Canham, Samuel; Woodcock, Jim
2
2015
Using formal reasoning on a model of tasks for FreeRTOS. Zbl 1328.68044
Cheng, Shu; Woodcock, Jim; D’Souza, Deepak
1
2015
CSP and Kripke structures. Zbl 1471.68135
Cavalcanti, Ana; Huang, Wen-ling; Peleska, Jan; Woodcock, Jim
1
2015
The safety-critical Java memory model formalised. Zbl 1259.68029
Cavalcanti, Ana; Wellings, Andy; Woodcock, Jim
6
2013
Unifying theories in ProofPower-Z. Zbl 1259.68035
Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim
6
2013
Circus Time with reactive designs. Zbl 1452.68057
Wei, Kun; Woodcock, Jim; Cavalcanti, Ana
5
2013
Safety-critical Java programs from Circus models. Zbl 1285.68037
Cavalcanti, Ana; Zeyda, Frank; Wellings, Andy; Woodcock, Jim; Wei, Kun
1
2013
Simulink timed models for program verification. Zbl 1390.68423
Cavalcanti, Ana; Mota, Alexandre; Woodcock, Jim
1
2013
Unifying theories of programming and formal engineering methods. International training school on software engineering, held at ICTAC 2013, Shanghai, China, August 26–30, 2013. Advanced lectures. Zbl 1320.68021
1
2013
Unifying theories of programming in Isabelle. Zbl 1444.68049
Foster, Simon; Woodcock, Jim
1
2013
The miracle of reactive programming. Zbl 1286.68096
Woodcock, Jim
6
2010
UTP semantics for Handel-C. Zbl 1286.68035
Perna, Juan Ignacio; Woodcock, Jim
4
2010
The tokeneer experiments. Zbl 1213.68391
Woodcock, Jim; Aydal, Emine Gökçe; Chapman, Rod
2
2010
Unifying theories of interrupts. Zbl 1286.68088
McEwan, Alistair A.; Woodcock, Jim
1
2010
A UTP semantics for Circus. Zbl 1165.68048
Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim
29
2009
POSIX file store in Z/Eves: An experiment in the verified software repository. Zbl 1162.68388
Freitas, Leo; Woodcock, Jim; Fu, Zheng
3
2009
Mechanising a formal model of flash memory. Zbl 1162.68387
Butterfield, Andrew; Freitas, Leo; Woodcock, Jim
2
2009
Mechanised wire-wise verification of Handel-C synthesis. Zbl 1347.68235
Perna, Juan Ignacio; Woodcock, Jim
1
2009
Formal methods: Foundations and applications. 12th Brazilian symposium on formal methods, SBMF 2009, Gramado, Brazil, August 19–21, 2009. Revised selected papers. Zbl 1177.68016
1
2009
A theory of pointers for the UTP. Zbl 1161.68388
Harwood, Will; Cavalcanti, Ana; Woodcock, Jim
13
2008
Proving theorems about JML classes. Zbl 1151.68348
Freitas, Leo; Woodcock, Jim
2
2007
Unifying theories in ProofPower-Z. Zbl 1186.68090
Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim
11
2006
Angelic nondeterminism in the unifying theories of programming. Zbl 1105.68012
Cavalcanti, Ana; Woodcock, Jim; Dunne, Steve
8
2006
Mechanising a unifying theory. Zbl 1186.68089
Nuka, Gift; Woodcock, Jim
7
2006
Z/Eves and the mondex electronic purse. Zbl 1168.68544
Woodcock, Jim; Freitas, Leo
5
2006
Pointers and records in the unifying theories of programming. Zbl 1186.68107
Cavalcanti, Ana; Harwood, Will; Woodcock, Jim
4
2006
The verified software repository: a step towards the verifying compiler. Zbl 1103.68452
Bicarregui, J. C.; Hoare, C. A. R.; Woodcock, J. C. P.
2
2006
Operational semantics for model checking Circus. Zbl 1120.68423
Woodcock, Jim; Cavalcanti, Ana; Freitas, Leonardo
6
2005
Angelic nondeterminism and unifying theories of programming. Zbl 1276.68054
Cavalcanti, Ana; Woodcock, Jim
2
2005
Simpler reasoning about system properties: a proof-by-refinement technique. Zbl 1276.68052
Atiya, D.; King, S.; Woodcock, J. C. P.
1
2005
A tutorial introduction to designs in unifying theories of programming. Zbl 1196.68031
Woodcock, Jim; Cavalcanti, Ana
9
2004
Travelling processes. Zbl 1106.68347
Tang, Xinbei; Woodcock, Jim
3
2004
A refinement strategy for Circus. Zbl 1093.68555
Cavalcanti, Ana; Sampaio, Augusto; Woodcock, Jim
23
2003
ArcAngel: a tactic language for refinement. Zbl 1093.68565
Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim
7
2003
Semantic domains for Handel-C. Zbl 1270.68151
Butterfield, Andrew; Woodcock, Jim
1
2003
The semantics of Circus. Zbl 1044.68560
Woodcock, Jim; Cavalcanti, Ana
22
2002
Refinement in Circus. Zbl 1064.68539
Sampaio, Augusto; Woodcock, Jim; Cavalcanti, Ana
6
2002
Unifying theories of parallel programming. Zbl 1015.68819
Woodcock, Jim; Hughes, Arthur
2
2002
REFINE 2002. Proceedings of the BCS FACS refinement workshop (satellite event of FLoC 2002), Copenhagen, Denmark, July 20–21, 2002. Zbl 1270.68022
1
2002
Refinement of actions in Circus. Zbl 1270.68079
Cavalcanti, Ana; Sampaio, Augusto; Woodcock, Jim
1
2002
On the refinement and simulation of data types and processes. Zbl 0963.68126
Bolton, Christie; Davies, Jim; Woodcock, Jim
7
1999
An inconsistency in procedures, parameters, and substitution in the refinement calculus. Zbl 0942.68014
Cavalcanti, Ana; Sampaio, Augusto; Woodcock, Jim
1
1999
FM ’99. Formal methods. World congress on Formal methods in the development of computing systems. Toulouse, France, September 20–24, 1999. Proceedings. In 2 vols. Zbl 0929.00076
1
1999
ZRC – A refinement calculus for \(Z\). Zbl 0934.68062
Cavalcanti, Ana; Woodcock, Jim
9
1998
A weakest precondition semantics for Z. Zbl 0906.68093
Cavalcanti, Ana; Woodcock, Jim
2
1998
Security management via \(Z\) and CSP. Zbl 0924.68139
Simpson, Andrew; Davies, Jim; Woodcock, Jim
1
1998
Using Z. Specification, refinement, and proof. Zbl 0855.68060
Woodcock, Jim; Davies, Jim
87
1996
A tactic calculus. — Abridged version. Zbl 0857.68094
Martin, A. P.; Gardiner, P. H. B.; Woodcock, J. C. P.
8
1996
Software engineering mathematics. Zbl 0825.68032
Woodcock, Jim; Loomes, Martin
2
1988
Transaction processing primitives and CSP. Zbl 0629.68018
Woodcock, J. C. P.
1
1987
all top 5

Cited by 241 Authors

32 Cavalcanti, Ana
28 Woodcock, James C. P.
12 Zeyda, Frank
10 Derrick, John
8 Foster, Simon
7 Boiten, Eerke A.
6 Freitas, Leo
6 Zhu, Huibiao
5 Butterfield, Andrew
5 Sampaio, Augusto C. A.
5 Schellhorn, Gerhard
5 Wehrheim, Heike
4 Bjørner, Dines
4 Hayes, Ian J.
4 Oliveira, Marcel
3 Banach, Richard
3 Brooke, Phillip J.
3 Colvin, Robert J.
3 Guttmann, Walter
3 Hallerstede, Stefan
3 Perna, Juan Ignacio
3 Qin, Shengchao
3 Reeves, Steve
3 Ribeiro, Pedro
3 Smith, Graeme
3 Streader, David
3 Wei, Kun
2 Bauer, Sebastian S.
2 Burns, Alan D.
2 Cornélio, Márcio
2 Cristiá, Maximiliano
2 da Costa, Umberto Souza
2 Dong, JinSong
2 Fu, Zheng
2 Gardiner, Paul H. B.
2 Gaudel, Marie-Claude
2 Gibbons, Jeremy
2 Gleirscher, Mario
2 He, Jifeng
2 Hennicker, Rolf
2 Hesselink, Wim H.
2 Hilscher, Martin
2 Jacob, Jeremy L.
2 Liu, Zhiming
2 Martins Moreira, Anamaria
2 Mota, Alexandre C.
2 Musicante, Martin A.
2 Ngondi, Gerard Ekembe
2 O’Halloran, Colin
2 Olderog, Ernst-Rüdiger
2 Oliveira, José Nuno
2 Paige, Richard F.
2 Ravn, Anders P.
2 Rossi, Gianfranco
2 Schwammberger, Maike
2 Souza Neto, Plácido A.
2 Struth, Georg
2 Sun, Jun
2 Treharne, Helen
2 Wellings, Andy
2 Wirsing, Martin
2 Wong, Peter Y. H.
2 Xie, Wanling
2 Zhan, Naijun
1 Aguirre, Nazareno M.
1 Alvaro, Peter
1 Amálio, Nuno
1 Ameloot, Tom J.
1 Andrews, Peter B.
1 Andronick, June
1 Armstrong, Alasdair
1 Aspinall, David
1 Banks, Michael J.
1 Barbosa, Luís Soares
1 Barnat, Jiří
1 Baxter, James
1 Berger, Martin J.
1 Berghammer, Rudolf
1 Börger, Egon
1 Boström, Pontus
1 Bowen, Jonathan P.
1 Boyer, Benoît
1 Bozzelli, Laura
1 Brien, S. M.
1 Brim, Luboš
1 Brown, Chad Edward
1 Brucker, Achim D.
1 Bundy, Alan
1 Calinescu, Radu C.
1 Canham, Samuel
1 Carvalho Júnior, Antonio
1 Castro, Pablo F.
1 Chen, Chunqing
1 Chen, Mingshuai
1 Chen, Zhenbang
1 Cheng, Shu
1 Chin, Wei-Ngan
1 Clayton, Phil
1 da Costa Cavalheiro, Simone André
1 Dang, Han-Hing
...and 141 more Authors

Citations by Year