Jim Woodcock

According to our database, Jim Woodcock authored at least 217 papers between 1987 and 2024.

Collaborative distances:

• Dijkstra number of two.
• Erdős number of four.

2024

Formally verified animation for RoboChart using interaction trees.

Kangfeng Ye, Simon Foster, Jim Woodcock

J. Log. Algebraic Methods Program., February, 2024

RoboCertProb: Property Specification for Probabilistic RoboChart Models.

Kangfeng Ye, Jim Woodcock

CoRR, 2024

2023

A manifesto for applicable formal methods.

Mario Gleirscher, Jaco van de Pol, Jim Woodcock

Softw. Syst. Model., December, 2023

Introduction to the Special Section on Reliability, Safety, and Security of Railway Systems.

Simon Collart Dutilleul, Anne E. Haxthausen, Thierry Lecomte, Jim Woodcock

Formal Aspects Comput., March, 2023

Trustworthy Autonomous Systems Through Verifiability.

Mohammad Reza Mousavi, Ana Cavalcanti, Michael Fisher, Louise A. Dennis, Robert M. Hierons, Bilal Y. Kaddouh, Effie Lai-Chong Law, Robert C. Richardson, Jan Oliver Ringert, Ivan Tyukin, Jim Woodcock

Computer, February, 2023

Checking and Automating Confidentiality Theory in Isabelle/UTP.

Lex Bailey, Jim Woodcock, Simon Foster, Roberto Metere

CoRR, 2023

State of the Art Report: Verified Computation.

Jim Woodcock, Mikkel Schimdt Andersen, Diego F. Aranha, Stefan Hallerstede, Simon Thrane Hansen, Nikolaj Kuhne Jakobsen, Tomas Kulik, Peter Gorm Larsen, Hugo Daniel Macedo, Carlos Ignacio Isasa Martin, Victor Alexander Mtsimbe Norrild

CoRR, 2023

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

Kangfeng Ye, Jim Woodcock, Simon Foster

CoRR, 2023

Modelling and Verifying Robotic Software that Uses Neural Networks.

Ziggy Attala, Ana Cavalcanti, Jim Woodcock

Proceedings of the Theoretical Aspects of Computing - ICTAC 2023, 2023

Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment.

Mustafa Adam, Kangfeng Ye, David A. Anisi, Ana Cavalcanti, Jim Woodcock, Robert Morris

Proceedings of the 19th IEEE International Conference on Automation Science and Engineering, 2023

Towards a Unifying Framework for Uncertainty in Cyber-Physical Systems.

Jim Woodcock

Proceedings of the Applicable Formal Methods for Safe Industrial Products, 2023

UTP, Circus, and Isabelle.

Jim Woodcock, Ana Cavalcanti, Simon Foster, Marcel Oliveira, Augusto Sampaio, Frank Zeyda

Proceedings of the Theories of Programming and Formal Methods, 2023

2022

Probabilistic modelling and verification using RoboChart and PRISM.

Kangfeng Ye, Ana Cavalcanti, Simon Foster, Alvaro Miyazawa, Jim Woodcock

Softw. Syst. Model., 2022

A Survey of Practical Formal Methods for Security.

Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter W. V. Tran-Jørgensen, Jim Woodcock

Formal Aspects Comput., 2022

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

Pedro Antonino, Augusto Sampaio, Jim Woodcock

CoRR, 2022

Formally Verified Self-adaptation of an Incubator Digital Twin.

Thomas Wright, Cláudio Gomes, Jim Woodcock

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Practice, 2022

Engineering of Digital Twins for Cyber-Physical Systems.

John S. Fitzgerald, Peter Gorm Larsen, Tiziana Margaria, Jim Woodcock, Cláudio Gomes

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Practice, 2022

2021

Automated verification of reactive and concurrent programs by calculation.

Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock

J. Log. Algebraic Methods Program., 2021

Learning safe neural network controllers with barrier certificates.

Hengjun Zhao, Xia Zeng, Taolue Chen, Zhiming Liu, Jim Woodcock

Formal Aspects Comput., 2021

RiskStructures: A design algebra for risk-aware machines.

Mario Gleirscher, Radu Calinescu, Jim Woodcock

Formal Aspects Comput., 2021

Editorial.

Alessandro Fantechi, Anne E. Haxthausen, Jim Woodcock

Formal Aspects Comput., 2021

Editorial.

Xiaoping Chen, Zhiming Liu, Ji Wang, Jim Woodcock

Formal Aspects Comput., 2021

Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps.

Simon Thrane Hansen, Cláudio Gomes, Maurizio Palmieri, Casper Thule, Jaco van de Pol, Jim Woodcock

Proceedings of the Formal Methods for Industrial Critical Systems, 2021

Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL.

Simon Foster, Chung-Kil Hur, Jim Woodcock

Proceedings of the 32nd International Conference on Concurrency Theory, 2021

Verification and Uncertainties in Self-integrating System.

Lukas Esterle, Barry Porter, Jim Woodcock

Proceedings of the IEEE International Conference on Autonomic Computing and Self-Organizing Systems, 2021

Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving.

Kangfeng Ye, Simon Foster, Jim Woodcock

Proceedings of the Relational and Algebraic Methods in Computer Science, 2021

Verification in the Grand Challenge.

Jim Woodcock, Janet Barnes, Rod Chapman, Simon Foster, Thomas Santen

Proceedings of the Theories of Programming: The Life and Works of Tony Hoare, 2021

Hoare and He's Unifying Theories of Programming.

Jim Woodcock

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.

Wanli Chang, Ran Wei, Shuai Zhao, Andy J. Wellings, Jim Woodcock, Alan Burns

ACM Trans. Embed. Comput. Syst., 2020

Unifying theories of reactive design contracts.

Simon Foster, Ana Cavalcanti, Samuel Canham, Jim Woodcock, Frank Zeyda

Theor. Comput. Sci., 2020

Unifying semantic foundations for automated verification tools in Isabelle/UTP.

Simon Foster, James Baxter, Ana Cavalcanti, Jim Woodcock, Frank Zeyda

Sci. Comput. Program., 2020

New Opportunities for Integrated Formal Methods.

Mario Gleirscher, Simon Foster, Jim Woodcock

ACM Comput. Surv., 2020

Uncertainty Quantification and Runtime Monitoring Using Environment-Aware Digital Twins.

Jim Woodcock, Cláudio Gomes, Hugo Daniel Macedo, Peter Gorm Larsen

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends, 2020

Engineering of Digital Twins for Cyber-Physical Systems.

John S. Fitzgerald, Peter Gorm Larsen, Tiziana Margaria, Jim Woodcock

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends, 2020

2019

RoboChart: modelling and verification of the functional behaviour of robotic applications.

Alvaro Miyazawa, Pedro Ribeiro, Wei Li, Ana Cavalcanti, Jon Timmis, Jim Woodcock

Softw. Syst. Model., 2019

Probabilistic Semantics for RoboChart - A Weakest Completion Approach.

Jim Woodcock, Ana Cavalcanti, Simon Foster, Alexandre Mota, Kangfeng Ye

Proceedings of the Unifying Theories of Programming - 7th International Symposium, 2019

A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic.

Tony Hoare, Georg Struth, Jim Woodcock

Proceedings of the Unifying Theories of Programming - 7th International Symposium, 2019

2018

Unifying theories of time with generalised reactive processes.

Simon Foster, Ana Cavalcanti, Jim Woodcock, Frank Zeyda

Inf. Process. Lett., 2018

Assuring Autonomous Systems: Opportunities for Integrated Formal Methods?

Mario Gleirscher, Simon Foster, Jim Woodcock

CoRR, 2018

Analysing RoboChart with Probabilities.

Madiel S. Conserva Filho, R. Marinho, Alexandre Mota, Jim Woodcock

Proceedings of the Formal Methods: Foundations and Applications - 21st Brazilian Symposium, 2018

Cyber-Physical Systems Engineering: An Introduction.

J. Paul Gibson, Peter Gorm Larsen, Marc Pantel, John S. Fitzgerald, Jim Woodcock

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.

Simon Foster, James Baxter, Ana Cavalcanti, Alvaro Miyazawa, Jim Woodcock

Proceedings of the Formal Aspects of Component Software - 15th International Conference, 2018

Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra.

Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock

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.

Kangfeng Ye, Jim Woodcock

Int. J. Softw. Tools Technol. Transf., 2017

Editorial.

Maurizio Proietti, Hirohisa Seki, Jim Woodcock

Formal Aspects Comput., 2017

Unifying Theories of Timed with Generalised Reactive Processes.

Simon Foster, Ana Cavalcanti, Jim Woodcock, Frank Zeyda

CoRR, 2017

What can agile methods bring to high-integrity software development?

Roderick Chapman, Neil White, Jim Woodcock

Commun. ACM, 2017

Features of Integrated Model-Based Co-modelling and Co-simulation Technology.

Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock, Carl Gamble, Richard John Payne, Kenneth Pierce

Proceedings of the Software Engineering and Formal Methods, 2017

Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL.

Simon Foster, Jim Woodcock

Proceedings of the Concurrency, Security, and Puzzles, 2017

Sound Simulation and Co-simulation for Robotics.

Ana Cavalcanti, Alvaro Miyazawa, Richard John Payne, Jim Woodcock

Proceedings of the Present and Ulterior Software Engineering., 2017

2016

A Stepwise Approach to Linking Theories.

Pedro Ribeiro, Ana Cavalcanti, Jim Woodcock

Proceedings of the Unifying Theories of Programming - 6th International Symposium, 2016

UTP Semantics of Reactive Processes with Continuations.

Gerard Ekembe Ngondi, Jim Woodcock

Proceedings of the Unifying Theories of Programming - 6th International Symposium, 2016

Towards a UTP Semantics for Modelica.

Simon Foster, Bernhard Thiele, Ana Cavalcanti, Jim Woodcock

Proceedings of the Unifying Theories of Programming - 6th International Symposium, 2016

UTP by Example: Designs.

Jim Woodcock, Simon Foster

Proceedings of the Engineering Trustworthy Software Systems - Second International School, 2016

Java in the Safety-Critical Domain.

Ana Cavalcanti, Alvaro Miyazawa, Andy J. Wellings, Jim Woodcock, Shuai Zhao

Proceedings of the Engineering Trustworthy Software Systems - Second International School, 2016

Heterogeneous Semantics and Unifying Theories.

Jim Woodcock, Simon Foster, Andrew Butterfield

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.

Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock, René A. Nilsson, Carl Gamble, Simon Foster

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Unifying Heterogeneous State-Spaces with Lenses.

Simon Foster, Frank Zeyda, Jim Woodcock

Proceedings of the Theoretical Aspects of Computing - ICTAC 2016, 2016

Behavioural Models for FMI Co-simulations.

Ana Cavalcanti, Jim Woodcock, Nuno Amálio

Proceedings of the Theoretical Aspects of Computing - ICTAC 2016, 2016

Checking SysML Models for Co-simulation.

Nuno Amálio, Richard John Payne, Ana Cavalcanti, Jim Woodcock

Proceedings of the Formal Methods and Software Engineering, 2016

From Formalised State Machines to Implementations of Robotic Controllers.

Wei Li, Alvaro Miyazawa, Pedro Ribeiro, Ana Cavalcanti, Jim Woodcock, Jon Timmis

Proceedings of the Distributed Autonomous Robotic Systems, 2016

Integrated tool chain for model-based design of Cyber-Physical Systems: The INTO-CPS project.

Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock, Peter Fritzson, Jörg Brauer, Christian Kleijn, Thierry Lecomte, Markus Pfeil, Ole Green, Stylianos Basagiannis, Andrey Sadovykh

Proceedings of the 2016 2nd International Workshop on Modelling, 2016

2015

Mechanised Theory Engineering in Isabelle.

Simon Foster, Jim Woodcock

Proceedings of the Dependable Software Systems Engineering, 2015

Model checking CML: tool development and industrial applications.

Alexandre Mota, Adalberto Farias, Jim Woodcock, Peter Gorm Larsen

Formal Aspects Comput., 2015

Using formal reasoning on a model of tasks for FreeRTOS.

Shu Cheng, Jim Woodcock, Deepak D'Souza

Formal Aspects Comput., 2015

Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions.

Claus Ballegaard Nielsen, Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock, Jan Peleska

ACM Comput. Surv., 2015

Mobile CSP.

Jim Woodcock, Andy J. Wellings, Ana Cavalcanti

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

CSP and Kripke Structures.

Ana Cavalcanti, Wen-ling Huang, Jan Peleska, Jim Woodcock

Proceedings of the Theoretical Aspects of Computing - ICTAC 2015, 2015

Cyber-Physical Systems Design: Formal Foundations, Methods and Integrated Tool Chains.

John S. Fitzgerald, Carl Gamble, Peter Gorm Larsen, Kenneth Pierce, Jim Woodcock

Proceedings of the 3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, 2015

Refinement-Based Verification of the FreeRTOS Scheduler in VCC.

Sumesh Divakaran, Deepak D'Souza, Anirudh Kushwah, Prahladavaradan Sampath, Nigamanth Sridhar, Jim Woodcock

Proceedings of the Formal Methods and Software Engineering, 2015

2014

Adapting FreeRTOS for multicores: an experience report.

James Mistry, Matthew Naylor, Jim Woodcock

Softw. Pract. Exp., 2014

Test-data generation for control coverage by proof.

Ana Cavalcanti, Steve King, Colin O'Halloran, Jim Woodcock

Formal Aspects Comput., 2014

Towards Algebraic Semantics of Circus Time.

Kun Wei, Jim Woodcock

Proceedings of the Unifying Theories of Programming - 5th International Symposium, 2014

Isabelle/UTP: A Mechanised Theory Engineering Framework.

Simon Foster, Frank Zeyda, Jim Woodcock

Proceedings of the Unifying Theories of Programming - 5th International Symposium, 2014

Three Approaches to Timed External Choice in UTP.

Samuel Canham, Jim Woodcock

Proceedings of the Unifying Theories of Programming - 5th International Symposium, 2014

An approach for managing semantic heterogeneity in Systems of Systems Engineering.

Simon Foster, Alvaro Miyazawa, Jim Woodcock, Ana Cavalcanti, John S. Fitzgerald, Peter Gorm Larsen

Proceedings of the 9th International Conference on System of Systems Engineering, 2014

Rapid Prototyping of a Semantically Well Founded Circus Model Checker.

Alexandre Mota, Adalberto Farias, André Didier, Jim Woodcock

Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

Contracts in CML.

Jim Woodcock, Ana Cavalcanti, John S. Fitzgerald, Simon Foster, Peter Gorm Larsen

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

Engineering UToPiA - Formal Semantics for CML.

Jim Woodcock

Proceedings of the FM 2014: Formal Methods, 2014

A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes.

Pedro R. G. Antonino, Augusto Sampaio, Jim Woodcock

Proceedings of the FM 2014: Formal Methods, 2014

2013

Safety-critical Java programs from Circus models.

Ana Cavalcanti, Frank Zeyda, Andy J. Wellings, Jim Woodcock, Kun Wei

Real Time Syst., 2013

Modelling temporal behaviour in complex systems with Timebands.

Kun Wei, Jim Woodcock, Alan Burns

Formal Methods Syst. Des., 2013

Unifying theories in ProofPower-Z.

Marcel Oliveira, Ana Cavalcanti, Jim Woodcock

Formal Aspects Comput., 2013

The Safety-Critical Java memory model formalised.

Ana Cavalcanti, Andy J. Wellings, Jim Woodcock

Formal Aspects Comput., 2013

A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP.

Marcel Vinícius Medeiros Oliveira, Ivan Soares de Medeiros Júnior, Jim Woodcock

Proceedings of the Software Engineering and Formal Methods - 11th International Conference, 2013

Unifying Theories of Logic and Specification.

Victor Bandur, Jim Woodcock

Proceedings of the Formal Methods: Foundations and Applications - 16th Brazilian Symposium, 2013

Unifying Theories of Programming in Isabelle.

Simon Foster, Jim Woodcock

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

Foundations for Model-Based Engineering of Systems of Systems.

John S. Fitzgerald, Peter Gorm Larsen, Jim Woodcock

Proceedings of the Complex Systems Design & Management, 2013

Simulink Timed Models for Program Verification.

Ana Cavalcanti, Alexandre Mota, Jim Woodcock

Proceedings of the Theories of Programming and Formal Methods, 2013

Industrial Deployment of Formal Methods: Trends and Challenges.

John S. Fitzgerald, Juan Bicarregui, Peter Gorm Larsen, Jim Woodcock

Proceedings of the Industrial Deployment of System Engineering Methods, 2013

2012

Editorial.

Jim Woodcock

Formal Aspects Comput., 2012

Unifying Theories of Undefinedness in UTP.

Jim Woodcock, Victor Bandur

Proceedings of the Unifying Theories of Programming, 4th International Symposium, 2012

<i>Circus Time</i> with Reactive Designs.

Kun Wei, Jim Woodcock, Ana Cavalcanti

Proceedings of the Unifying Theories of Programming, 4th International Symposium, 2012

Features of CML: A formal modelling language for Systems of Systems.

Jim Woodcock, Ana Cavalcanti, John S. Fitzgerald, Peter Gorm Larsen, Alvaro Miyazawa, Simon Perry

Proceedings of the 7th International Conference on System of Systems Engineering, 2012

A Plug-in Based Approach for UML Model Simulation.

Alek Radjenovic, Richard F. Paige, Louis M. Rose, Jim Woodcock, Steve King

Proceedings of the Modelling Foundations and Applications - 8th European Conference, 2012

Modelling Temporal Behaviour in Complex Systems with Timebands.

Kun Wei, Jim Woodcock, Alan Burns

Proceedings of the Conquering Complexity, 2012

2011

Editorial.

Zhiming Liu, Jim Woodcock

Formal Aspects Comput., 2011

Editorial.

Daniel Kroening, Tiziana Margaria, Jim Woodcock

Formal Aspects Comput., 2011

Correct hardware synthesis - An algebraic approach.

Juan Ignacio Perna, Jim Woodcock, Augusto Sampaio, Juliano Iyoda

Acta Informatica, 2011

Safety-critical Java in Circus.

Ana Cavalcanti, Andy J. Wellings, Jim Woodcock, Kun Wei, Frank Zeyda

Proceedings of the 9th International Workshop on Java Technologies for Real-time and Embedded Systems, 2011

Timed Circus: Timed CSP with the Miracle.

Kun Wei, Jim Woodcock, Alan Burns

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.

Osmar Marchi dos Santos, Jim Woodcock, Richard F. Paige

Proceedings of the 16th IEEE International Conference on Engineering of Complex Computer Systems, 2011

The Safety-Critical Java Memory Model: A Formal Account.

Ana Cavalcanti, Andy J. Wellings, Jim Woodcock

Proceedings of the FM 2011: Formal Methods, 2011

2010

Programming Phase: Formal Methods.

Richard F. Paige, Jim Woodcock, Phillip J. Brooke, Ana Cavalcanti

Proceedings of the Encyclopedia of Software Engineering, 2010

Considering Software Preservation.

Brian Matthews, Arif Shaon, Juan Bicarregui, Catherine Mary Jones, Esther Conway, Jim Woodcock

ERCIM News, 2010

Modelling and Implementing Complex Systems with Timebands.

Jim Woodcock, Marcel Oliveira, Alan Burns, Kun Wei

Proceedings of the Fourth International Conference on Secure Software Integration and Reliability Improvement, 2010

A Timed Model of Circus with the Reactive Design Miracle.

Kun Wei, Jim Woodcock, Alan Burns

Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, 2010

The Tokeneer Experiments.

Jim Woodcock, Emine Gökçe Aydal, Rod Chapman

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.

Leo Freitas, Jim Woodcock, Yichi Zhang

Sci. Comput. Program., 2009

POSIX file store in Z/Eves: An experiment in the verified software repository.

Leo Freitas, Jim Woodcock, Zheng Fu

Sci. Comput. Program., 2009

Mechanising a formal model of flash memory.

Andrew Butterfield, Leo Freitas, Jim Woodcock

Sci. Comput. Program., 2009

A Chain Datatype in Z.

Leo Freitas, Jim Woodcock

Int. J. Softw. Informatics, 2009

Editorial.

Richard F. Paige, Phillip J. Brooke, Jin Song Dong, J. C. P. Woodcock

Formal Aspects Comput., 2009

A UTP semantics for <i>Circus</i>.

Marcel Oliveira, Ana Cavalcanti, Jim Woodcock

Formal Aspects Comput., 2009

Formal methods: Practice and experience.

Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, John S. Fitzgerald

ACM Comput. Surv., 2009

State Visibility and Communication in Unifying Theories of Programming.

Andrew Butterfield, Pawel Gancarski, Jim Woodcock

Proceedings of the TASE 2009, 2009

Towards a Methodology for Software Preservation.

Brian Matthews, Esther Conway, Jim Woodcock, Catherine Mary Jones, Juan Bicarregui, Arif Shaon

Proceedings of the 6th International Conference on Digital Preservation, 2009

Putting Formal Specifications under the Magnifying Glass: Model-based Testing for Validation.

Emine Gokce Aydal, Richard F. Paige, Mark Utting, Jim Woodcock

Proceedings of the Second International Conference on Software Testing Verification and Validation, 2009

The Use of Model Transformation in the INESS Project.

Osmar Marchi dos Santos, Jim Woodcock, Richard F. Paige, Steve King

Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

Industrial Practice in Formal Methods: A Review.

Juan Bicarregui, John S. Fitzgerald, Peter Gorm Larsen, J. C. P. Woodcock

Proceedings of the FM 2009: Formal Methods, 2009

09381 Extended Abstracts Collection - Refinement Based Methods for the Construction of Dependable Systems.

Jean-Raymond Abrial, Michael J. Butler, Rajev Joshi, Elena Troubitsyna, J. C. P. Woodcock

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.

Jim Woodcock, Susan Stepney, David Cooper, John A. Clark, Jeremy Jacob

Formal Aspects Comput., 2008

Editorial.

Cliff B. Jones, Jim Woodcock

Formal Aspects Comput., 2008

Mechanising Mondex with Z/Eves.

Leo Freitas, Jim Woodcock

Formal Aspects Comput., 2008

Mechanised Wire-wise Verification of Handel-C Synthesis.

Juan Ignacio Perna, Jim Woodcock

Proceedings of the Eleventh Brazilian Symposium on Formal Methods, 2008

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

Emine Gokce Aydal, Richard F. Paige, Jim Woodcock

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2008

The Miracle of Reactive Programming.

Jim Woodcock

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

UTP Semantics for Handel-C.

Juan Ignacio Perna, Jim Woodcock

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

Unifying Theories of Interrupts.

Alistair A. McEwan, Jim Woodcock

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

A Comparison of State-Based Modelling Tools for Model Validation.

Emine Gokce Aydal, Mark Utting, Jim Woodcock

Proceedings of the Objects, Components, Models and Patterns, 46th International Conference, 2008

A Theory of Pointers for the UTP.

Will Harwood, Ana Cavalcanti, Jim Woodcock

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.

Emine Gokce Aydal, Richard F. Paige, Jim Woodcock

Proceedings of the First International Conference on Software Testing Verification and Validation, 2008

Linking VDM and Z.

Jim Woodcock, Leo Freitas

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.

Leo Freitas, Jim Woodcock, Andrew Butterfield

Proceedings of the 13th International Conference on Engineering of Complex Computer Systems (ICECCS 2008), March 31 2008, 2008

ABZ2008 VSR-Net Workshop.

Jim Woodcock, Paul Boca

Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

2007

The Verification Grand Challenge.

Jim Woodcock, Richard Banach

J. Univers. Comput. Sci., 2007

Slotted-Circus.

Andrew Butterfield, Adnan Sherif, Jim Woodcock

Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Goal-Oriented Automatic Test Case Generators for MC/DC Compliancy.

Emine Gokce Aydal, Jim Woodcock, Ana Cavalcanti

Proceedings of the ICSOFT 2007, 2007

A Denotational Semantics for Handel-C Hardware Compilation.

Juan Ignacio Perna, Jim Woodcock

Proceedings of the Formal Methods and Software Engineering, 2007

Automatic Generation of Verified Concurrent Hardware.

Marcel Oliveira, Jim Woodcock

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.

Leo Freitas, Konstantinos Mokos, Jim Woodcock

Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

Formalising Flash Memory: First Steps.

Andrew Butterfield, Jim Woodcock

Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

Proving Theorems About JML Classes.

Leo Freitas, Jim Woodcock

Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007

2006

State-rich model checking.

Leo Freitas, Jim Woodcock, Ana Cavalcanti

Innov. Syst. Softw. Eng., 2006

Angelic nondeterminism in the unifying theories of programming.

Ana Cavalcanti, Jim Woodcock, Steve Dunne

Formal Aspects Comput., 2006

The verified software repository: a step towards the verifying compiler.

Juan Bicarregui, C. A. R. Hoare, J. C. P. Woodcock

Formal Aspects Comput., 2006

A Denotational Semantics for Circus.

Marcel Oliveira, Ana Cavalcanti, Jim Woodcock

Proceedings of the 11th Refinement Workshop, 2006

FDR Explorer.

Leo Freitas, Jim Woodcock

Proceedings of the 11th Refinement Workshop, 2006

First Steps in the Verified Software Grand Challenge.

Jim Woodcock

Computer, 2006

Verified Software: A Grand Challenge.

Cliff B. Jones, Peter W. O'Hearn, Jim Woodcock

Computer, 2006

An Operational Semantics in UTP for a Language of Reactive Designs (Abstract).

Jim Woodcock

Proceedings of the Unifying Theories of Programming, First International Symposium, 2006

Mechanising a Unifying Theory.

Gift Nuka, Jim Woodcock

Proceedings of the Unifying Theories of Programming, First International Symposium, 2006

Pointers and Records in the Unifying Theories of Programming.

Ana Cavalcanti, Will Harwood, Jim Woodcock

Proceedings of the Unifying Theories of Programming, First International Symposium, 2006

Z/Eves and the Mondex Electronic Purse.

Jim Woodcock, Leo Freitas

Proceedings of the Theoretical Aspects of Computing, 2006

Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking.

Leo Freitas, Ana Cavalcanti, Jim Woodcock

Proceedings of the Formal Methods and Software Engineering, 2006

A Layered Behavioural Model of Platelets.

Steve A. Schneider, Helen Treharne, Ana Cavalcanti, Jim Woodcock

Proceedings of the 11th International Conference on Engineering of Complex Computer Systems (ICECCS 2006), 2006

Verified Software Grand Challenge.

Jim Woodcock

Proceedings of the FM 2006: Formal Methods, 2006

2005

prialt in Handel-C: an operational semantics.

Andrew Butterfield, Jim Woodcock

Int. J. Softw. Tools Technol. Transf., 2005

Unifying classes and processes.

Ana Cavalcanti, Augusto Sampaio, Jim Woodcock

Softw. Syst. Model., 2005

Formal development of industrial-scale systems in <i>Circus</i>.

Marcel Oliveira, Ana Cavalcanti, Jim Woodcock

Innov. Syst. Softw. Eng., 2005

Angelic Nondeterminism and Unifying Theories of Programming.

Ana Cavalcanti, Jim Woodcock

Proceedings of the REFINE 2005 Workshop, 2005

Simpler Reasoning About System Properties: a Proof-by-Refinement Technique.

Diyaa-Addein Atiya, Steve King, Jim Woodcock

Proceedings of the REFINE 2005 Workshop, 2005

Operational Semantics for Model Checking Circus.

Jim Woodcock, Ana Cavalcanti, Leonardo Freitas

Proceedings of the FM 2005: Formal Methods, 2005

Unifying Program Refinement Calculi.

Jim Woodcock

Proceedings of the 12th International Workshop on Abstract State Machines, 2005

2004

A "Hardware Compiler" Semantics for Handel-C.

Andrew Butterfield, Jim Woodcock

Proceedings of the Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, 2004

Towards Mobile Processes in Unifying Theories.

Xinbei Tang, Jim Woodcock

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>.

Ana Cavalcanti, Jim Woodcock

Proceedings of the Refinement Techniques in Software Engineering, 2004

Refinement: An overview.

Ana Cavalcanti, Augusto Sampaio, Jim Woodcock

Proceedings of the Refinement Techniques in Software Engineering, 2004

Travelling Processes.

Xinbei Tang, Jim Woodcock

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

A Tutorial Introduction to Designs in Unifying Theories of Programming.

Jim Woodcock, Ana Cavalcanti

Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

A refinement based approach to calculating a fault tolerant railway signal device.

Alistair A. McEwan, J. C. P. Woodcock

Proceedings of the Building the Information Society, 2004

2003

Predicate transformers in the semantics of Circus.

Ana Cavalcanti, Jim Woodcock

IEE Proc. Softw., 2003

ArcAngel: a Tactic Language for Refinement.

Marcel Oliveira, Ana Cavalcanti, Jim Woodcock

Formal Aspects Comput., 2003

A Refinement Strategy for Circus.

Ana Cavalcanti, Augusto Sampaio, Jim Woodcock

Formal Aspects Comput., 2003

Using Circus for Safety-critical Applications.

Jim Woodcock

Proceedings of the 6th Brazilian Workshop on Formal Methods, 2003

Mechanising the Alphabetised Relational Calculus.

Gift Nuka, Jim Woodcock

Proceedings of the 6th Brazilian Workshop on Formal Methods, 2003

An Operational Semantics for Handel-C.

Andrew Butterfield, Jim Woodcock

Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems, 2003

A Circus Semantics for Ravenscar Protected Objects.

Diyaa-Addein Atiya, Steve King, Jim Woodcock

Proceedings of the FME 2003: Formal Methods, 2003

2002

Preface.

John Derrick, Eerke A. Boiten, Jim Woodcock, Joakim von Wright

Proceedings of the BCS FACS Refinement Workshop 2002, 2002

Refinement of actions in Circus.

Ana Cavalcanti, Augusto Sampaio, Jim Woodcock

Proceedings of the BCS FACS Refinement Workshop 2002, 2002

Semantic domains for Handel-C.

Andrew Butterfield, Jim Woodcock

Proceedings of the Second Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, 2002

The Semantics of Circus.

Jim Woodcock, Ana Cavalcanti

Proceedings of the ZB 2002: Formal Specification and Development in Z and B, 2002

Unifying Theories of Parallel Programming.

Jim Woodcock, Arthur P. Hughes

Proceedings of the Formal Methods and Software Engineering, 2002

Refinement in Circus.

Augusto Sampaio, Jim Woodcock, Ana Cavalcanti

Proceedings of the FME 2002: Formal Methods, 2002

2001

A Concurrent Language for Refinement.

Jim Woodcock, Ana Cavalcanti

Proceedings of the 5th Irish Workshop on Formal Methods, 2001

The Steam Boiler in a Unified Theory of Z and CSP.

Jim Woodcock, Ana Cavalcanti

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.

Jeannette M. Wing, Jim Woodcock

IEEE Trans. Software Eng., 2000

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

Jeannette M. Wing, Jim Woodcock

Formal Methods Syst. Des., 2000

The First World Congress on Formal Methods in the Development of Computing Systems.

Jeannette M. Wing, Jim Woodcock

Formal Aspects Comput., 2000

1999

An Inconsistency in Procedures, Parameters, and Substitution in the Refinement Calculus.

Ana Cavalcanti, Augusto Sampaio, Jim Woodcock

Sci. Comput. Program., 1999

When to Trust Mobile Objects: Access Control in the Jini(tm) Software System.

Charles Crichton, Jim Davies, Jim Woodcock

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.

Christie Bolton, Jim Davies, Jim Woodcock

Proceedings of the Integrated Formal Methods, 1999

1998

Procedures and Recursion in the Refinement Calculus.

Ana Cavalcanti, Augusto Sampaio, Jim Woodcock

J. Braz. Comput. Soc., 1998

ZRC - A Refinement Calculus for Z.

Ana Cavalcanti, Jim Woodcock

Formal Aspects Comput., 1998

A Weakest Precondition Semantics for Z.

Ana Cavalcanti, Jim Woodcock

Comput. J., 1998

More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement.

Susan Stepney, David Cooper, Jim Woodcock

Proceedings of the ZUM '98: The Z Formal Specification Notation, 1998

Safety through Security.

Andrew Simpson, Jim Woodcock, Jim Davies

Proceedings of the 9th International Workshop on Software Specification and Design, 1998

1996

Non-interference through Determinism.

A. W. Roscoe, Jim Woodcock, Lars Wulf

J. Comput. Secur., 1996

A Tactic Calculus-Abridged Version.

Andrew P. Martin, Paul H. B. Gardiner, Jim Woodcock

Formal Aspects Comput., 1996

Software Engineering Research Directions.

Jim Woodcock

ACM Comput. Surv., 1996

Using Z - specification, refinement, and proof.

J. C. P. Woodcock, Jim Davies

Prentice Hall international series in computer science, Prentice Hall, ISBN: 978-0-13-948472-8, 1996

1995

Introduction to Special Section (Guest Editorial).

Jim Woodcock, Peter Gorm Larsen

IEEE Trans. Software Eng., 1995

Event Refinement in State-Based Concurrent Systems.

Jane E. Sinclair, Jim Woodcock

Formal Aspects Comput., 1995

1994

The Formal Specification in Z of Defence Standard 00-56.

Jim Woodcock, Paul H. B. Gardiner, J. R. Hulance

Proceedings of the Z User Workshop, Cambridge, UK, 29-30 June 1994, Proceedings, 1994

1992

The Rudiments of Algorithm Refinement.

Jim Woodcock

Comput. J., 1992

Implementing Promoted Operations in Z.

J. C. P. Woodcock

Proceedings of the 5th Refinement Workshop, 1992

1991

Two Refinement Case Studies.

Jim Woodcock

Proceedings of the VDM '91, 1991

An Introduction to Refinement in Z.

Jim Woodcock

Proceedings of the VDM '91, 1991

The Refinement Calculus.

Jim Woodcock

Proceedings of the VDM '91, 1991

A Tutorial on the Refinement Calculus.

Jim Woodcock

Proceedings of the VDM '91, 1991

1990

A Simpler Semantics for Z.

Paul H. B. Gardiner, P. J. Lupton, Jim Woodcock

Proceedings of the Z User Workshop, 1990

Refinement of State-Based Concurrent Systems.

Jim Woodcock, Carroll Morgan

Proceedings of the VDM '90, 1990

1989

Properties of Z specifications.

J. C. P. Woodcock

ACM SIGSOFT Softw. Eng. Notes, 1989

Structuring specifications in Z.

J. C. P. Woodcock

Softw. Eng. J., 1989

1988

Formalisms.

J. C. P. Woodcock

ACM SIGSOFT Softw. Eng. Notes, 1988

Using VDM with Rely and Guarantee-Conditions - Experiences from a Real Project.

Jim Woodcock, B. Dickinson

Proceedings of the VDM '88, 1988

1987

Towards the formal specification of a simple programming support environment.

Bernard Sufrin, Jim Woodcock

Softw. Eng. J., 1987