Jim Woodcock

Orcid: 0000-0001-7955-2702

Affiliations:
  • University of York, Department of Computer Science, UK


According to our database1, Jim Woodcock authored at least 222 papers between 1987 and 2024.

Collaborative distances:
  • Dijkstra number2 of two.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Formal design, verification and implementation of robotic controller software via RoboChart and RoboTool.
Auton. Robots, August, 2024

Formally verified animation for RoboChart using interaction trees.
J. Log. Algebraic Methods Program., February, 2024

Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: Semantics and automated reasoning with theorem proving.
Theor. Comput. Sci., 2024

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL.
CoRR, 2024

RoboCertProb: Property Specification for Probabilistic RoboChart Models.
CoRR, 2024

Digital Twin Engineering.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Application Areas, 2024

2023
A manifesto for applicable formal methods.
Softw. Syst. Model., December, 2023

Introduction to the Special Section on Reliability, Safety, and Security of Railway Systems.
Formal Aspects Comput., March, 2023

Trustworthy Autonomous Systems Through Verifiability.
Computer, February, 2023

Checking and Automating Confidentiality Theory in Isabelle/UTP.
CoRR, 2023

State of the Art Report: Verified Computation.
CoRR, 2023

Probabilistic relations for modelling epistemic and aleatoric uncertainty: its semantics and automated reasoning with theorem proving.
CoRR, 2023

Modelling and Verifying Robotic Software that Uses Neural Networks.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2023, 2023

Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment.
Proceedings of the 19th IEEE International Conference on Automation Science and Engineering, 2023

Towards a Unifying Framework for Uncertainty in Cyber-Physical Systems.
Proceedings of the Applicable Formal Methods for Safe Industrial Products, 2023

UTP, Circus, and Isabelle.
Proceedings of the Theories of Programming and Formal Methods, 2023

2022
Probabilistic modelling and verification using RoboChart and PRISM.
Softw. Syst. Model., 2022

A Survey of Practical Formal Methods for Security.
Formal Aspects Comput., 2022

A Pattern-based deadlock-freedom analysis strategy for concurrent systems.
CoRR, 2022

Formally Verified Self-adaptation of an Incubator Digital Twin.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Practice, 2022

Engineering of Digital Twins for Cyber-Physical Systems.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Practice, 2022

2021
Automated verification of reactive and concurrent programs by calculation.
J. Log. Algebraic Methods Program., 2021

Learning safe neural network controllers with barrier certificates.
Formal Aspects Comput., 2021

RiskStructures: A design algebra for risk-aware machines.
Formal Aspects Comput., 2021

Editorial.
Formal Aspects Comput., 2021

Editorial.
Formal Aspects Comput., 2021

Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps.
Proceedings of the Formal Methods for Industrial Critical Systems, 2021

Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL.
Proceedings of the 32nd International Conference on Concurrency Theory, 2021

Verification and Uncertainties in Self-integrating System.
Proceedings of the IEEE International Conference on Autonomic Computing and Self-Organizing Systems, 2021

Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving.
Proceedings of the Relational and Algebraic Methods in Computer Science, 2021

Verification in the Grand Challenge.
Proceedings of the Theories of Programming: The Life and Works of Tony Hoare, 2021

Hoare and He's Unifying Theories of Programming.
Proceedings of the Theories of Programming: The Life and Works of Tony Hoare, 2021

2020
Development Automation of Real-Time Java: Model-Driven Transformation and Synthesis.
ACM Trans. Embed. Comput. Syst., 2020

Unifying theories of reactive design contracts.
Theor. Comput. Sci., 2020

Unifying semantic foundations for automated verification tools in Isabelle/UTP.
Sci. Comput. Program., 2020

New Opportunities for Integrated Formal Methods.
ACM Comput. Surv., 2020

Uncertainty Quantification and Runtime Monitoring Using Environment-Aware Digital Twins.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends, 2020

Engineering of Digital Twins for Cyber-Physical Systems.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends, 2020

2019
Automated Verification of Reactive and Concurrent Programs by Calculation, supporting material.
Dataset, November, 2019

RoboChart: modelling and verification of the functional behaviour of robotic applications.
Softw. Syst. Model., 2019

Probabilistic Semantics for RoboChart - A Weakest Completion Approach.
Proceedings of the Unifying Theories of Programming - 7th International Symposium, 2019

A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic.
Proceedings of the Unifying Theories of Programming - 7th International Symposium, 2019

2018
Unifying theories of time with generalised reactive processes.
Inf. Process. Lett., 2018

Assuring Autonomous Systems: Opportunities for Integrated Formal Methods?
CoRR, 2018

Analysing RoboChart with Probabilities.
Proceedings of the Formal Methods: Foundations and Applications - 21st Brazilian Symposium, 2018

Cyber-Physical Systems Engineering: An Introduction.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, 2018

Automating Verification of State Machines with Reactive Designs and Isabelle/UTP.
Proceedings of the Formal Aspects of Component Software - 15th International Conference, 2018

Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra.
Proceedings of the Relational and Algebraic Methods in Computer Science, 2018

2017
Model checking of state-rich formalism <i>Circus</i> by linking to CSP ‖ B.
Int. J. Softw. Tools Technol. Transf., 2017

Editorial.
Formal Aspects Comput., 2017

Unifying Theories of Timed with Generalised Reactive Processes.
CoRR, 2017

What can agile methods bring to high-integrity software development?
Commun. ACM, 2017

Features of Integrated Model-Based Co-modelling and Co-simulation Technology.
Proceedings of the Software Engineering and Formal Methods, 2017

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

Sound Simulation and Co-simulation for Robotics.
Proceedings of the Present and Ulterior Software Engineering., 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

From Formalised State Machines to Implementations of Robotic Controllers.
Proceedings of the Distributed Autonomous Robotic Systems, 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

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

Using formal reasoning on a model of tasks for FreeRTOS.
Formal Aspects 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. Exp., 2014

Test-data generation for control coverage by proof.
Formal Aspects 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 Syst., 2013

Modelling temporal behaviour in complex systems with Timebands.
Formal Methods Syst. Des., 2013

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

The Safety-Critical Java memory model formalised.
Formal Aspects 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 Aspects Comput., 2012

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

<i>Circus Time</i> 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 Aspects Comput., 2011

Editorial.
Formal Aspects Comput., 2011

Correct hardware synthesis - An algebraic approach.
Acta Informatica, 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. Softw. Informatics, 2009

Editorial.
Formal Aspects Comput., 2009

A UTP semantics for <i>Circus</i>.
Formal Aspects Comput., 2009

FDR Explorer.
Formal Aspects Comput., 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

Towards a Methodology for Software Preservation.
Proceedings of the 6th International Conference on Digital Preservation, 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 Aspects Comput., 2008

Editorial.
Formal Aspects Comput., 2008

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

Evaluation of OCL for Large-Scale Modelling: A Different View of the Mondex Purse.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 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. Univers. Comput. Sci., 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

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.
Innov. Syst. Softw. Eng., 2006

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

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

A Denotational Semantics for Circus.
Proceedings of the 11th Refinement Workshop, 2006

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

Verified Software: A Grand Challenge.
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

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

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.
Int. J. Softw. Tools Technol. Transf., 2005

Unifying classes and processes.
Softw. Syst. Model., 2005

Formal development of industrial-scale systems in <i>Circus</i>.
Innov. Syst. Softw. Eng., 2005

Angelic Nondeterminism and Unifying Theories of Programming.
Proceedings of the REFINE 2005 Workshop, 2005

Simpler Reasoning About System Properties: a Proof-by-Refinement Technique.
Proceedings of the REFINE 2005 Workshop, 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
A "Hardware Compiler" Semantics for Handel-C.
Proceedings of the Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, 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 <i>Unifying Theories of Programming</i>.
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 Proc. Softw., 2003

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

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

Using Circus for Safety-critical Applications.
Proceedings of the 6th Brazilian Workshop on Formal Methods, 2003

Mechanising the Alphabetised Relational Calculus.
Proceedings of the 6th Brazilian Workshop on Formal Methods, 2003

An Operational Semantics for Handel-C.
Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems, 2003

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

2002
Preface.
Proceedings of the BCS FACS Refinement Workshop 2002, 2002

Refinement of actions in Circus.
Proceedings of the BCS FACS Refinement Workshop 2002, 2002

Semantic domains for Handel-C.
Proceedings of the Second Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, 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 Syst. Des., 2000

The First World Congress on Formal Methods in the Development of Computing Systems.
Formal Aspects 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. Comput. Soc., 1998

ZRC - A Refinement Calculus for Z.
Formal Aspects 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

Safety through Security.
Proceedings of the 9th International Workshop on Software Specification and Design, 1998

1996
Non-interference through Determinism.
J. Comput. Secur., 1996

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

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

Using Z - specification, refinement, and proof.
Prentice Hall international series in computer science, Prentice Hall, ISBN: 978-0-13-948472-8, 1996

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

Event Refinement in State-Based Concurrent Systems.
Formal Aspects 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

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

Implementing Promoted Operations in Z.
Proceedings of the 5th Refinement Workshop, 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
Properties of Z specifications.
ACM SIGSOFT Softw. Eng. Notes, 1989

Structuring specifications in Z.
Softw. Eng. J., 1989

1988
Formalisms.
ACM SIGSOFT Softw. Eng. Notes, 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.
Softw. Eng. J., 1987


  Loading...