Jim Woodcock

According to our database1, Jim Woodcock
  • authored at least 173 papers between 1987 and 2017.
  • has a "Dijkstra number"2 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2017
Model checking of state-rich formalism Circus by linking to CSP ‖ B.
STTT, 2017

Editorial.
Formal Asp. Comput., 2017

From Formalised State Machines to Implementations of Robotic Controllers.
CoRR, 2017

Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL.
Proceedings of the Concurrency, Security, and Puzzles, 2017

2016
A Stepwise Approach to Linking Theories.
Proceedings of the Unifying Theories of Programming - 6th International Symposium, 2016

UTP Semantics of Reactive Processes with Continuations.
Proceedings of the Unifying Theories of Programming - 6th International Symposium, 2016

Towards a UTP Semantics for Modelica.
Proceedings of the Unifying Theories of Programming - 6th International Symposium, 2016

UTP by Example: Designs.
Proceedings of the Engineering Trustworthy Software Systems - Second International School, 2016

Java in the Safety-Critical Domain.
Proceedings of the Engineering Trustworthy Software Systems - Second International School, 2016

Heterogeneous Semantics and Unifying Theories.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016

Towards Semantically Integrated Models and Tools for Cyber-Physical Systems Design.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Unifying Heterogeneous State-Spaces with Lenses.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2016, 2016

Behavioural Models for FMI Co-simulations.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2016, 2016

Checking SysML Models for Co-simulation.
Proceedings of the Formal Methods and Software Engineering, 2016

Integrated tool chain for model-based design of Cyber-Physical Systems: The INTO-CPS project.
Proceedings of the 2016 2nd International Workshop on Modelling, 2016

2015
Mechanised Theory Engineering in Isabelle.
Proceedings of the Dependable Software Systems Engineering, 2015

Editorial.
Formal Asp. Comput., 2015

Model checking CML: tool development and industrial applications.
Formal Asp. Comput., 2015

Using formal reasoning on a model of tasks for FreeRTOS.
Formal Asp. Comput., 2015

Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions.
ACM Comput. Surv., 2015

Mobile CSP.
Proceedings of the Formal Methods: Foundations and Applications - 18th Brazilian Symposium, 2015

CSP and Kripke Structures.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2015, 2015

Cyber-Physical Systems Design: Formal Foundations, Methods and Integrated Tool Chains.
Proceedings of the 3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, 2015

Refinement-Based Verification of the FreeRTOS Scheduler in VCC.
Proceedings of the Formal Methods and Software Engineering, 2015

2014
Adapting FreeRTOS for multicores: an experience report.
Softw., Pract. Exper., 2014

Test-data generation for control coverage by proof.
Formal Asp. Comput., 2014

Towards Algebraic Semantics of Circus Time.
Proceedings of the Unifying Theories of Programming - 5th International Symposium, 2014

Isabelle/UTP: A Mechanised Theory Engineering Framework.
Proceedings of the Unifying Theories of Programming - 5th International Symposium, 2014

Three Approaches to Timed External Choice in UTP.
Proceedings of the Unifying Theories of Programming - 5th International Symposium, 2014

An approach for managing semantic heterogeneity in Systems of Systems Engineering.
Proceedings of the 9th International Conference on System of Systems Engineering, 2014

Rapid Prototyping of a Semantically Well Founded Circus Model Checker.
Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

Contracts in CML.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014

Engineering UToPiA - Formal Semantics for CML.
Proceedings of the FM 2014: Formal Methods, 2014

A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes.
Proceedings of the FM 2014: Formal Methods, 2014

2013
Safety-critical Java programs from Circus models.
Real-Time Systems, 2013

Modelling temporal behaviour in complex systems with Timebands.
Formal Methods in System Design, 2013

Unifying theories in ProofPower-Z.
Formal Asp. Comput., 2013

The Safety-Critical Java memory model formalised.
Formal Asp. Comput., 2013

A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP.
Proceedings of the Software Engineering and Formal Methods - 11th International Conference, 2013

Unifying Theories of Logic and Specification.
Proceedings of the Formal Methods: Foundations and Applications - 16th Brazilian Symposium, 2013

Unifying Theories of Programming in Isabelle.
Proceedings of the Unifying Theories of Programming and Formal Engineering Methods, 2013

Foundations for Model-Based Engineering of Systems of Systems.
Proceedings of the Complex Systems Design & Management, 2013

Simulink Timed Models for Program Verification.
Proceedings of the Theories of Programming and Formal Methods, 2013

Industrial Deployment of Formal Methods: Trends and Challenges.
Proceedings of the Industrial Deployment of System Engineering Methods, 2013

2012
Mechanised wire-wise verification of Handel-C synthesis.
Sci. Comput. Program., 2012

Editorial.
Formal Asp. Comput., 2012

Unifying Theories of Undefinedness in UTP.
Proceedings of the Unifying Theories of Programming, 4th International Symposium, 2012

Circus Time with Reactive Designs.
Proceedings of the Unifying Theories of Programming, 4th International Symposium, 2012

Features of CML: A formal modelling language for Systems of Systems.
Proceedings of the 7th International Conference on System of Systems Engineering, 2012

A Plug-in Based Approach for UML Model Simulation.
Proceedings of the Modelling Foundations and Applications - 8th European Conference, 2012

Modelling Temporal Behaviour in Complex Systems with Timebands.
Proceedings of the Conquering Complexity, 2012

2011
Editorial.
Formal Asp. Comput., 2011

Editorial.
Formal Asp. Comput., 2011

Correct hardware synthesis - An algebraic approach.
Acta Inf., 2011

Safety-critical Java in Circus.
Proceedings of the 9th International Workshop on Java Technologies for Real-time and Embedded Systems, 2011

Timed Circus: Timed CSP with the Miracle.
Proceedings of the 16th IEEE International Conference on Engineering of Complex Computer Systems, 2011

Using Model Transformation to Generate Graphical Counter-Examples for the Formal Analysis of xUML Models.
Proceedings of the 16th IEEE International Conference on Engineering of Complex Computer Systems, 2011

The Safety-Critical Java Memory Model: A Formal Account.
Proceedings of the FM 2011: Formal Methods, 2011

2010
Programming Phase: Formal Methods.
Proceedings of the Encyclopedia of Software Engineering, 2010

Considering Software Preservation.
ERCIM News, 2010

Modelling and Implementing Complex Systems with Timebands.
Proceedings of the Fourth International Conference on Secure Software Integration and Reliability Improvement, 2010

A Timed Model of Circus with the Reactive Design Miracle.
Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, 2010

The Tokeneer Experiments.
Proceedings of the Reflections on the Work of C. A. R. Hoare., 2010

2009
Verifying the CICS File Control API with Z/Eves: An experiment in the verified software repository.
Sci. Comput. Program., 2009

POSIX file store in Z/Eves: An experiment in the verified software repository.
Sci. Comput. Program., 2009

Mechanising a formal model of flash memory.
Sci. Comput. Program., 2009

A Chain Datatype in Z.
Int. J. Software and Informatics, 2009

Editorial.
Formal Asp. Comput., 2009

A UTP semantics for Circus.
Formal Asp. Comput., 2009

FDR Explorer.
Formal Asp. Comput., 2009

Mechanised Wire-wise Verification of Handel-C Synthesis.
Electr. Notes Theor. Comput. Sci., 2009

Formal methods: Practice and experience.
ACM Comput. Surv., 2009

State Visibility and Communication in Unifying Theories of Programming.
Proceedings of the TASE 2009, 2009

Putting Formal Specifications under the Magnifying Glass: Model-based Testing for Validation.
Proceedings of the Second International Conference on Software Testing Verification and Validation, 2009

The Use of Model Transformation in the INESS Project.
Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

Industrial Practice in Formal Methods: A Review.
Proceedings of the FM 2009: Formal Methods, 2009

09381 Extended Abstracts Collection - Refinement Based Methods for the Construction of Dependable Systems.
Proceedings of the Refinement Based Methods for the Construction of Dependable Systems, 13.09., 2009

2008
The certification of the Mondex electronic purse to ITSEC Level E6.
Formal Asp. Comput., 2008

Editorial.
Formal Asp. Comput., 2008

Mechanising Mondex with Z/Eves.
Formal Asp. Comput., 2008

Evaluation of OCL for Large-Scale Modelling: A Different View of the Mondex Purse.
ECEASST, 2008

The Miracle of Reactive Programming.
Proceedings of the Unifying Theories of Programming, Second International Symposium, 2008

UTP Semantics for Handel-C.
Proceedings of the Unifying Theories of Programming, Second International Symposium, 2008

Unifying Theories of Interrupts.
Proceedings of the Unifying Theories of Programming, Second International Symposium, 2008

A Comparison of State-Based Modelling Tools for Model Validation.
Proceedings of the Objects, Components, Models and Patterns, 46th International Conference, 2008

A Theory of Pointers for the UTP.
Proceedings of the Theoretical Aspects of Computing, 2008

Observations for Assertion-based Scenarios in the context of Model Validation and Extension to Test Case Generation.
Proceedings of the First International Conference on Software Testing Verification and Validation, 2008

Linking VDM and Z.
Proceedings of the 13th International Conference on Engineering of Complex Computer Systems (ICECCS 2008), March 31 2008, 2008

POSIX and the Verification Grand Challenge: A Roadmap.
Proceedings of the 13th International Conference on Engineering of Complex Computer Systems (ICECCS 2008), March 31 2008, 2008

ABZ2008 VSR-Net Workshop.
Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

2007
The Verification Grand Challenge.
J. UCS, 2007

Editorial.
Formal Asp. Comput., 2007

A Denotational Semantics for Circus.
Electr. Notes Theor. Comput. Sci., 2007

FDR Explorer.
Electr. Notes Theor. Comput. Sci., 2007

Evaluation of OCL for Large-Scale Modelling: A Different View of the Mondex Purse.
Proceedings of the Models in Software Engineering, Workshops and Symposia at MoDELS 2007, Nashville, TN, USA, September 30, 2007

Slotted-Circus.
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Goal-Oriented Automatic Test Case Generators for MC/DC Compliancy.
Proceedings of the ICSOFT 2007, 2007

A Denotational Semantics for Handel-C Hardware Compilation.
Proceedings of the Formal Methods and Software Engineering, 2007

Automatic Generation of Verified Concurrent Hardware.
Proceedings of the Formal Methods and Software Engineering, 2007

Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository.
Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

POSIX file store in Z/Eves: an experiment in the verified software repository.
Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

Formalising Flash Memory: First Steps.
Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

Proving Theorems About JML Classes.
Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007

2006
State-rich model checking.
ISSE, 2006

Angelic nondeterminism in the unifying theories of programming.
Formal Asp. Comput., 2006

The verified software repository: a step towards the verifying compiler.
Formal Asp. Comput., 2006

A "Hardware Compiler" Semantics for Handel-C.
Electr. Notes Theor. Comput. Sci., 2006

First Steps in the Verified Software Grand Challenge.
IEEE Computer, 2006

Verified Software: A Grand Challenge.
IEEE Computer, 2006

An Operational Semantics in UTP for a Language of Reactive Designs (Abstract).
Proceedings of the Unifying Theories of Programming, First International Symposium, 2006

Unifying Theories in ProofPower-Z.
Proceedings of the Unifying Theories of Programming, First International Symposium, 2006

Mechanising a Unifying Theory.
Proceedings of the Unifying Theories of Programming, First International Symposium, 2006

Pointers and Records in the Unifying Theories of Programming.
Proceedings of the Unifying Theories of Programming, First International Symposium, 2006

First Steps in the Verified Software Grand Challenge.
Proceedings of the 30th Annual IEEE / NASA Software Engineering Workshop (SEW-30 2006), 2006

Z/Eves and the Mondex Electronic Purse.
Proceedings of the Theoretical Aspects of Computing, 2006

Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking.
Proceedings of the Formal Methods and Software Engineering, 2006

A Layered Behavioural Model of Platelets.
Proceedings of the 11th International Conference on Engineering of Complex Computer Systems (ICECCS 2006), 2006

Verified Software Grand Challenge.
Proceedings of the FM 2006: Formal Methods, 2006

2005
prialt in Handel-C: an operational semantics.
STTT, 2005

Unifying classes and processes.
Software and System Modeling, 2005

Formal development of industrial-scale systems in Circus.
ISSE, 2005

Angelic Nondeterminism and Unifying Theories of Programming.
Electr. Notes Theor. Comput. Sci., 2005

Simpler Reasoning About System Properties: a Proof-by-Refinement Technique.
Electr. Notes Theor. Comput. Sci., 2005

Operational Semantics for Model Checking Circus.
Proceedings of the FM 2005: Formal Methods, 2005

Unifying Program Refinement Calculi.
Proceedings of the 12th International Workshop on Abstract State Machines, 2005

2004
Using Circus for Safety-critical Applications.
Electr. Notes Theor. Comput. Sci., 2004

Mechanising the Alphabetised Relational Calculus.
Electr. Notes Theor. Comput. Sci., 2004

Towards Mobile Processes in Unifying Theories.
Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

A Tutorial Introduction to CSP in Unifying Theories of Programming.
Proceedings of the Refinement Techniques in Software Engineering, 2004

Refinement: An overview.
Proceedings of the Refinement Techniques in Software Engineering, 2004

Travelling Processes.
Proceedings of the Mathematics of Program Construction, 7th International Conference, 2004

A Tutorial Introduction to Designs in Unifying Theories of Programming.
Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

A refinement based approach to calculating a fault tolerant railway signal device.
Proceedings of the Building the Information Society, 2004

2003
Predicate transformers in the semantics of Circus.
IEE Proceedings - Software, 2003

ArcAngel: a Tactic Language for Refinement.
Formal Asp. Comput., 2003

A Refinement Strategy for Circus.
Formal Asp. Comput., 2003

An Operational Semantics for Handel-C.
Electr. Notes Theor. Comput. Sci., 2003

A Circus Semantics for Ravenscar Protected Objects.
Proceedings of the FME 2003: Formal Methods, 2003

2002
Preface.
Electr. Notes Theor. Comput. Sci., 2002

Refinement of actions in Circus.
Electr. Notes Theor. Comput. Sci., 2002

Semantic domains for Handel-C.
Electr. Notes Theor. Comput. Sci., 2002

The Semantics of Circus.
Proceedings of the ZB 2002: Formal Specification and Development in Z and B, 2002

Unifying Theories of Parallel Programming.
Proceedings of the Formal Methods and Software Engineering, 2002

Refinement in Circus.
Proceedings of the FME 2002: Formal Methods, 2002

2001
A Concurrent Language for Refinement.
Proceedings of the 5th Irish Workshop on Formal Methods, 2001

The Steam Boiler in a Unified Theory of Z and CSP.
Proceedings of the 8th Asia-Pacific Software Engineering Conference (APSEC 2001), 2001

2000
Guest Editors' Introduction-Special Issues for FM '99: The First World Congress On Formal Methods in the Development of Computing Systems.
IEEE Trans. Software Eng., 2000

Introduction: Special Issues for FM'99, the First World Congress on Formal Methods in the Development of Computing Systems.
Formal Methods in System Design, 2000

The First World Congress on Formal Methods in the Development of Computing Systems.
Formal Asp. Comput., 2000

1999
An Inconsistency in Procedures, Parameters, and Substitution in the Refinement Calculus.
Sci. Comput. Program., 1999

When to Trust Mobile Objects: Access Control in the Jini(tm) Software System.
Proceedings of the TOOLS 1999: 30th International Conference on Technology of Object-Oriented Languages and Systems, Delivering Quality Software, 1999

On the Refinement and Simulation of Data Types and Processes.
Proceedings of the Integrated Formal Methods, 1999

1998
Procedures and Recursion in the Refinement Calculus.
J. Braz. Comp. Soc., 1998

ZRC - A Refinement Calculus for Z.
Formal Asp. Comput., 1998

A Weakest Precondition Semantics for Z.
Comput. J., 1998

More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement.
Proceedings of the ZUM '98: The Z Formal Specification Notation, 1998

1996
Non-interference through Determinism.
Journal of Computer Security, 1996

A Tactic Calculus-Abridged Version.
Formal Asp. Comput., 1996

Software Engineering Research Directions.
ACM Comput. Surv., 1996

1995
Introduction to Special Section (Guest Editorial).
IEEE Trans. Software Eng., 1995

Event Refinement in State-Based Concurrent Systems.
Formal Asp. Comput., 1995

1994
The Formal Specification in Z of Defence Standard 00-56.
Proceedings of the Z User Workshop, Cambridge, UK, 29-30 June 1994, Proceedings, 1994

Non-Interference Through Determinism.
Proceedings of the Computer Security, 1994

1992
The Rudiments of Algorithm Refinement.
Comput. J., 1992

1991
Two Refinement Case Studies.
Proceedings of the VDM '91, 1991

An Introduction to Refinement in Z.
Proceedings of the VDM '91, 1991

The Refinement Calculus.
Proceedings of the VDM '91, 1991

A Tutorial on the Refinement Calculus.
Proceedings of the VDM '91, 1991

1990
A Simpler Semantics for Z.
Proceedings of the Z User Workshop, 1990

Refinement of State-Based Concurrent Systems.
Proceedings of the VDM '90, 1990

1989
Structuring specifications in Z.
Software Engineering Journal, 1989

1988
Using VDM with Rely and Guarantee-Conditions - Experiences from a Real Project.
Proceedings of the VDM '88, 1988

1987
Towards the formal specification of a simple programming support environment.
Software Engineering Journal, 1987


  Loading...