| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Jim Woodcock |
Editorial.  |
Formal Asp. Comput.  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Juan Ignacio Perna, Jim Woodcock |
Mechanised wire-wise verification of Handel-C synthesis. |
Sci. Comput. Program. |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhiming Liu, Jim Woodcock |
Editorial. |
Formal Asp. Comput. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Tiziana Margaria, Jim Woodcock |
Editorial. |
Formal Asp. Comput. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Juan Ignacio Perna, Jim Woodcock, Augusto Sampaio, Juliano Iyoda |
Correct hardware synthesis - An algebraic approach. |
Acta Inf. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, Andy J. Wellings, Jim Woodcock |
The Safety-Critical Java Memory Model: A Formal Account. |
FM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Osmar Marchi dos Santos, Jim Woodcock, Richard F. Paige |
Using Model Transformation to Generate Graphical Counter-Examples for the Formal Analysis of xUML Models. |
ICECCS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Kun Wei, Jim Woodcock, Alan Burns |
Timed Circus: Timed CSP with the Miracle. |
ICECCS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Brian Matthews, Arif Shaon, Juan Bicarregui, Catherine Jones, Esther Conway, Jim Woodcock |
Considering Software Preservation. |
ERCIM News |
2010 |
DBLP BibTeX RDF |
|
| 1 | Richard F. Paige, Jim Woodcock, Phillip J. Brooke, Ana Cavalcanti |
Programming Phase: Formal Methods. |
Encyclopedia of Software Engineering |
2010 |
DBLP BibTeX RDF |
|
| 1 | Kun Wei, Jim Woodcock, Alan Burns |
A Timed Model of Circus with the Reactive Design Miracle. |
SEFM |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel, Jim Woodcock (eds.) |
Theoretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010. Proceedings |
ICTAC |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Paulo Borba, Ana Cavalcanti, Augusto Sampaio, Jim Woodcock (eds.) |
Testing Techniques in Software Engineering, Second Pernambuco Summer School on Software Engineering, PSSE 2007, Recife, Brazil, December 3-7, 2007, Revised Lectures |
PSSE |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock, Marcel Oliveira, Alan Burns, Kun Wei |
Modelling and Implementing Complex Systems with Timebands. |
SSIRI |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Juan Bicarregui, John S. Fitzgerald, Peter Gorm Larsen, J. C. P. Woodcock |
Industrial Practice in Formal Methods: A Review. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Marcel Oliveira, Ana Cavalcanti, Jim Woodcock |
A UTP semantics for Circus. |
Formal Asp. Comput. |
2009 |
DBLP DOI BibTeX RDF |
Concurrency, Theorem proving, Relational model, Refinement calculus |
| 1 | Leo Freitas, Jim Woodcock |
FDR Explorer. |
Formal Asp. Comput. |
2009 |
DBLP DOI BibTeX RDF |
Model checking, Refinement, CSP, Automata, Labelled transition systems, FDR |
| 1 | Leo Freitas, Jim Woodcock |
A Chain Datatype in Z. |
Int. J. Software and Informatics |
2009 |
DBLP BibTeX RDF |
|
| 1 | Leo Freitas, Jim Woodcock, Yichi Zhang |
Verifying the CICS File Control API with Z/Eves: An experiment in the verified software repository. |
Sci. Comput. Program. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Butterfield, Leo Freitas, Jim Woodcock |
Mechanising a formal model of flash memory. |
Sci. Comput. Program. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Leo Freitas, Jim Woodcock, Zheng Fu |
POSIX file store in Z/Eves: An experiment in the verified software repository. |
Sci. Comput. Program. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Juan Ignacio Perna, Jim Woodcock |
Mechanised Wire-wise Verification of Handel-C Synthesis. |
Electr. Notes Theor. Comput. Sci. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, John S. Fitzgerald |
Formal methods: Practice and experience. |
ACM Comput. Surv. |
2009 |
DBLP DOI BibTeX RDF |
formal methods surveys, verified software initiative, grand challenges, Experimental software engineering, verified software repository |
| 1 | Emine G. Aydal, Richard F. Paige, Mark Utting, Jim Woodcock |
Putting Formal Specifications under the Magnifying Glass: Model-based Testing for Validation. |
ICST |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Osmar Marchi dos Santos, Jim Woodcock, Richard F. Paige, Steve King |
The Use of Model Transformation in the INESS Project. |
FMCO |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Marcel Vinicius Medeiros Oliveira, Jim Woodcock (eds.) |
Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers |
SBMF |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Butterfield, Pawel Gancarski, Jim Woodcock |
State Visibility and Communication in Unifying Theories of Programming. |
TASE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Emine G. Aydal, Richard F. Paige, Jim Woodcock |
Evaluation of OCL for Large-Scale Modelling: A Different View of the Mondex Purse. |
ECEASST |
2008 |
DBLP BibTeX RDF |
|
| 1 | Cliff B. Jones, Jim Woodcock |
Editorial. |
Formal Asp. Comput. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock, Susan Stepney, David Cooper, John A. Clark, Jeremy Jacob |
The certification of the Mondex electronic purse to ITSEC Level E6. |
Formal Asp. Comput. |
2008 |
DBLP DOI BibTeX RDF |
Electronic finance, Grand Challenge in Verified Software, ITSEC Level E6, Security, Verification, Refinement, Theorem proving, Smart cards, Certification, Correctness, Z notation, Grand challenges, Verified Software Repository, Mondex |
| 1 | Leo Freitas, Jim Woodcock |
Mechanising Mondex with Z/Eves. |
Formal Asp. Comput. |
2008 |
DBLP DOI BibTeX RDF |
Electronic finance, Grand Challenge in Verified Software, Software archaeology, Z/Eves, Security, Verification, Refinement, Theorem proving, Smart cards, Correctness, Z notation, Grand challenges, Verified Software Repository, Mondex |
| 1 | Emine G. Aydal, Mark Utting, Jim Woodcock |
A Comparison of State-Based Modelling Tools for Model Validation. |
TOOLS |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Will Harwood, Ana Cavalcanti, Jim Woodcock |
A Theory of Pointers for the UTP. |
ICTAC |
2008 |
DBLP DOI BibTeX RDF |
semantics, refinement, object models, relations |
| 1 | Bertrand Meyer, Jim Woodcock (eds.) |
Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar, Jim Woodcock (eds.) |
Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings |
VSTTE |
2008 |
DBLP BibTeX RDF |
|
| 1 | Alistair A. McEwan, Jim Woodcock |
Unifying Theories of Interrupts. |
UTP |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Juan Ignacio Perna, Jim Woodcock |
UTP Semantics for Handel-C. |
UTP |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock |
The Miracle of Reactive Programming. |
UTP |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Leo Freitas, Jim Woodcock, Andrew Butterfield |
POSIX and the Verification Grand Challenge: A Roadmap. |
ICECCS |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock, Leo Freitas |
Linking VDM and Z. |
ICECCS |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock, Paul Boca |
ABZ2008 VSR-Net Workshop. |
ABZ |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Cliff B. Jones, Jim Woodcock |
Editorial. |
Formal Asp. Comput. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock, Richard Banach |
The Verification Grand Challenge. |
J. UCS |
2007 |
DBLP BibTeX RDF |
|
| 1 | Marcel Oliveira, Ana Cavalcanti, Jim Woodcock |
A Denotational Semantics for Circus. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Leo Freitas, Jim Woodcock |
FDR Explorer. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Emine G. Aydal, Jim Woodcock, Ana Cavalcanti |
Goal-Oriented Automatic Test Case Generators for MC/DC Compliancy. |
ICSOFT (SE) |
2007 |
DBLP BibTeX RDF |
|
| 1 | Juan Ignacio Perna, Jim Woodcock |
A Denotational Semantics for Handel-C Hardware Compilation. |
ICFEM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Marcel Oliveira, Jim Woodcock |
Automatic Generation of Verified Concurrent Hardware. |
ICFEM |
2007 |
DBLP DOI BibTeX RDF |
FPGA, concurrency, refinement, CSP, tool support, program development, Handel-C, automatic compilation |
| 1 | Cliff B. Jones, Zhiming Liu, Jim Woodcock (eds.) |
Theoretical Aspects of Computing - ICTAC 2007, 4th International Colloquium, Macau, China, September 26-28, 2007, Proceedings |
ICTAC |
2007 |
DBLP BibTeX RDF |
|
| 1 | Andrew Butterfield, Adnan Sherif, Jim Woodcock |
Slotted-Circus. |
IFM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Emine G. Aydal, Richard F. Paige, Jim Woodcock |
Evaluation of OCL for Large-Scale Modelling: A Different View of the Mondex Purse. |
MoDELS Workshops |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Cliff B. Jones, Zhiming Liu, Jim Woodcock (eds.) |
Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007 |
Formal Methods and Hybrid Real-Time Systems |
2007 |
DBLP BibTeX RDF |
|
| 1 | Leo Freitas, Jim Woodcock |
Proving Theorems About JML Classes. |
Formal Methods and Hybrid Real-Time Systems |
2007 |
DBLP DOI BibTeX RDF |
Grand Challenge in Verified Software, Java Collections Framework, Java HashMap class, linking theories, Z/Eves, formal specification, Z, software verification, JML, Java Modeling Language, mechanical theorem proving, Verified Software Repository |
| 1 | Andrew Butterfield, Jim Woodcock |
Formalising Flash Memory: First Steps. |
ICECCS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Leo Freitas, Konstantinos Mokos, Jim Woodcock |
Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository. |
ICECCS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Leo Freitas, Zheng Fu, Jim Woodcock |
POSIX file store in Z/Eves: an experiment in the verified software repository. |
ICECCS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Chris George, Zhiming Liu, Jim Woodcock (eds.) |
Domain Modeling and the Duration Calculus, International Training School, Shanghai, China, September 17-21. 2007, Advanced Lectures |
Domain Modeling and the Duration Calculus |
2007 |
DBLP BibTeX RDF |
|
| 1 | Juan Bicarregui, C. A. R. Hoare, J. C. P. Woodcock |
The verified software repository: a step towards the verifying compiler. |
Formal Asp. Comput. |
2006 |
DBLP DOI BibTeX RDF |
Grand challenges in computer science, Dependable systems evolution, Software engineering, Tools, Program verification, Verified software repository, Verifying compiler, Assertional reasoning |
| 1 | Ana Cavalcanti, Jim Woodcock, Steve Dunne |
Angelic nondeterminism in the unifying theories of programming. |
Formal Asp. Comput. |
2006 |
DBLP DOI BibTeX RDF |
Semantics, Refinement, Relations, Predicate transformers |
| 1 | Leo Freitas, Jim Woodcock, Ana Cavalcanti |
State-rich model checking. |
ISSE |
2006 |
DBLP DOI BibTeX RDF |
Formal method tools, Model checking, Theorem proving, Abstract interpretation |
| 1 | Andrew Butterfield, Jim Woodcock |
A "Hardware Compiler" Semantics for Handel-C. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Cliff B. Jones, Peter W. O'Hearn, Jim Woodcock |
Verified Software: A Grand Challenge. |
IEEE Computer |
2006 |
DBLP DOI BibTeX RDF |
Verification Challenge, Formal methods, Software technologies |
| 1 | Jim Woodcock |
First Steps in the Verified Software Grand Challenge. |
IEEE Computer |
2006 |
DBLP DOI BibTeX RDF |
verified software grand challenge, software engineering |
| 1 | Leo Freitas, Ana Cavalcanti, Jim Woodcock |
Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking. |
ICFEM |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock, Leo Freitas |
Z/Eves and the Mondex Electronic Purse. |
ICTAC |
2006 |
DBLP DOI BibTeX RDF |
electronic finance, software archaeology, the Z notation, Z/Eves, security, refinement, theorem proving, smart cards, Grand Challenge, Verified Software Repository, Mondex |
| 1 | Jim Woodcock |
First Steps in the Verified Software Grand Challenge. |
SEW |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock |
Verified Software Grand Challenge. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Marcel Oliveira, Ana Cavalcanti, Jim Woodcock |
Unifying Theories in ProofPower-Z. |
UTP |
2006 |
DBLP DOI BibTeX RDF |
Unifying Theories of Programming, theorem prover |
| 1 | Ana Cavalcanti, Will Harwood, Jim Woodcock |
Pointers and Records in the Unifying Theories of Programming. |
UTP |
2006 |
DBLP DOI BibTeX RDF |
semantics, refinement, object models, relations |
| 1 | Jim Woodcock |
An Operational Semantics in UTP for a Language of Reactive Designs (Abstract). |
UTP |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Gift Nuka, Jim Woodcock |
Mechanising a Unifying Theory. |
UTP |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, Augusto Sampaio, Jim Woodcock (eds.) |
Refinement Techniques in Software Engineering, First Pernambuco Summer School on Software Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004, Revised Lectures |
PSSE |
2006 |
DBLP BibTeX RDF |
|
| 1 | Steve Schneider, Helen Treharne, Ana Cavalcanti, Jim Woodcock |
A Layered Behavioural Model of Platelets. |
ICECCS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, Augusto Sampaio, Jim Woodcock |
Unifying classes and processes. |
Software and System Modeling |
2005 |
DBLP DOI BibTeX RDF |
Integration, Refinement, CSP, Z |
| 1 | Marcel Oliveira, Ana Cavalcanti, Jim Woodcock |
Formal development of industrial-scale systems in Circus. |
ISSE |
2005 |
DBLP DOI BibTeX RDF |
Concurrency, Object-orientation, Refinement, Program development |
| 1 | Diyaa-Addein Atiya, Steve King, Jim Woodcock |
Simpler Reasoning About System Properties: a Proof-by-Refinement Technique. |
Electr. Notes Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, Jim Woodcock |
Angelic Nondeterminism and Unifying Theories of Programming. |
Electr. Notes Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Butterfield, Jim Woodcock |
prialt in Handel-C: an operational semantics. |
STTT |
2005 |
DBLP DOI BibTeX RDF |
Operational semantics, Priority, Handel-C |
| 1 | Jim Woodcock, Ana Cavalcanti, Leonardo Freitas |
Operational Semantics for Model Checking Circus. |
FM |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock |
Unifying Program Refinement Calculi. |
Abstract State Machines |
2005 |
DBLP BibTeX RDF |
|
| 1 | Alistair A. McEwan, J. C. P. Woodcock |
A refinement based approach to calculating a fault tolerant railway signal device. |
IFIP Congress Topical Sessions |
2004 |
DBLP BibTeX RDF |
|
| 1 | Gift Nuka, Jim Woodcock |
Mechanising the Alphabetised Relational Calculus. |
Electr. Notes Theor. Comput. Sci. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock |
Using Circus for Safety-critical Applications. |
Electr. Notes Theor. Comput. Sci. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Xinbei Tang, Jim Woodcock |
Towards Mobile Processes in Unifying Theories. |
SEFM |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock, Ana Cavalcanti |
A Tutorial Introduction to Designs in Unifying Theories of Programming. |
IFM |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, Augusto Sampaio, Jim Woodcock |
Refinement: An overview. |
PSSE |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, Jim Woodcock |
A Tutorial Introduction to CSP in Unifying Theories of Programming. |
PSSE |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Xinbei Tang, Jim Woodcock |
Travelling Processes. |
MPC |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Marcel Oliveira, Ana Cavalcanti, Jim Woodcock |
ArcAngel: a Tactic Language for Refinement. |
Formal Asp. Comput. |
2003 |
DBLP DOI BibTeX RDF |
ensp, Formal methods, Refinement calculus, Program development |
| 1 | Ana Cavalcanti, Augusto Sampaio, Jim Woodcock |
A Refinement Strategy for Circus. |
Formal Asp. Comput. |
2003 |
DBLP DOI BibTeX RDF |
Concurrency, CSP, Z, Program development |
| 1 | Andrew Butterfield, Jim Woodcock |
An Operational Semantics for Handel-C. |
Electr. Notes Theor. Comput. Sci. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, Jim Woodcock |
Predicate transformers in the semantics of Circus. |
IEE Proceedings - Software |
2003 |
DBLP BibTeX RDF |
|
| 1 | Jin Song Dong, Jim Woodcock (eds.) |
Formal Methods and Software Engineering, 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003, Proceedings |
ICFEM |
2003 |
DBLP BibTeX RDF |
|
| 1 | Diyaa-Addein Atiya, Steve King, Jim Woodcock |
A Circus Semantics for Ravenscar Protected Objects. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Ravenscar, Ada Protected Objects, Formal Semantics, Z, Circus |
| 1 | John Derrick, Eerke A. Boiten, Jim Woodcock, Joakim von Wright |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Butterfield, Jim Woodcock |
Semantic domains for Handel-C. |
Electr. Notes Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, Augusto Sampaio, Jim Woodcock |
Refinement of actions in Circus. |
Electr. Notes Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock, Arthur P. Hughes |
Unifying Theories of Parallel Programming. |
ICFEM |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock, Ana Cavalcanti |
The Semantics of Circus. |
ZB |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Augusto Sampaio, Jim Woodcock, Ana Cavalcanti |
Refinement in Circus. |
FME |
2002 |
DBLP DOI BibTeX RDF |
unifying theories of programming, distribution, CSP, Z |
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")