Jim Woodcock - RankMe

273 papers A 2B 24C 25Misc 3Journal 109Unranked 86

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects. CoRR Chao Wang, Ruijia Li, Yang Zhou, Peng Wu, Yi Lv, Jianwei Liao, Jim Woodcock, Zhiming Liu
2026	J	`jnl`	Jean-Raymond Abrial (1938 - 2025) Pioneer of Formal Methods and Inventor of the B Method. An Obituary. Formal Aspects Comput. Jim Woodcock
2025	J	`jnl`	Auto-Encoding Neural Tucker Factorization. IEEE Trans. Knowl. Data Eng. Peng Tang, Xin Luo, Jim Woodcock
2025	J	`jnl`	Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem. CoRR Dustin Bryant, Jim Woodcock, Simon Foster
2025	—	`conf`	Formal Verification of BDI Agents. The Combined Power of Research, Education, and Dissemination Thomas Wright, Louise A. Dennis, Jim Woodcock, Simon Foster
2025	J	`jnl`	Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version). CoRR Kangfeng Ye, Roberto Metere, Jim Woodcock, Poonam Yadav
2025	C	`conf`	Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks. ICFEM Kangfeng Ye, Roberto Metere, Jim Woodcock, Poonam Yadav
2025	J	`jnl`	In Memoriam: Ernest Allen Emerson II. Formal Aspects Comput. Jim Woodcock
2025	J	`jnl`	Probabilistic modelling and safety assurance of an agriculture robot providing light-treatment. CoRR Mustafa Adam, Kangfeng Ye, David A. Anisi, Ana Cavalcanti, Jim Woodcock, Robert Morris
2025	—	`conf`	Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software. NFM Ziggy Attala, Fang Yan, Simon Foster, Ana Cavalcanti, Jim Woodcock
2025	J	`jnl`	Software Engineering for Self-Adaptive Robotics: A Research Agenda. CoRR Shaukat Ali, Ana Cavalcanti, Cláudio Ângelo Gonçalves Gomes, Peter Gorm Larsen, Hassan Sartaj, Anastasios Tefas, Jim Woodcock, Houxiang Zhang
2025	J	`jnl`	The Sigmoid Function and the Universal Approximation Theorem. Arch. Formal Proofs Dustin Bryant, Jim Woodcock, Simon Foster
2025	J	`jnl`	Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL. ACM Trans. Softw. Eng. Methodol. Simon Foster, Chung-Kil Hur, Jim Woodcock
2025	J	`jnl`	Z Mathematical Toolkit in Isabelle/HOL. Arch. Formal Proofs Simon Foster, Pedro Ribeiro, Frank Zeyda, Jim Woodcock
2024	—	`conf`	Digital Twin Engineering. ISoLA (5) John S. Fitzgerald, Cláudio Gomes, Einar Broch Johnsen, Eduard Kamburjan, Martin Leucker, Jim Woodcock
2024	J	`jnl`	Formal design, verification and implementation of robotic controller software via RoboChart and RoboTool. Auton. Robots Wei Li, Pedro Ribeiro, Alvaro Miyazawa, Richard Redpath, Ana Cavalcanti, Kieran Alden, Jim Woodcock, Jon Timmis
2024	J	`jnl`	Formally verified animation for RoboChart using interaction trees. J. Log. Algebraic Methods Program. Kangfeng Ye, Simon Foster, Jim Woodcock
2024	—	`conf`	From Logic to Programming. SETSS Zhiming Liu, Jim Woodcock, Jonathan P. Bowen
2024	J	`jnl`	Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: Semantics and automated reasoning with theorem proving. Theor. Comput. Sci. Kangfeng Ye, Jim Woodcock, Simon Foster
2024	J	`jnl`	RoboCertProb: Property Specification for Probabilistic RoboChart Models. CoRR Kangfeng Ye, Jim Woodcock
2024	—	`ch.`	Uncertainty and Probabilistic UTP. The Practice of Formal Methods (II) Jim Woodcock
2024	J	`jnl`	Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL. CoRR Simon Foster, Chung-Kil Hur, Jim Woodcock
2023	J	`jnl`	A manifesto for applicable formal methods. Softw. Syst. Model. Mario Gleirscher, Jaco van de Pol, Jim Woodcock
2023	J	`jnl`	Checking and Automating Confidentiality Theory in Isabelle/UTP. CoRR Lex Bailey, Jim Woodcock, Simon Foster, Roberto Metere
2023	J	`jnl`	Formally Verified Animation for RoboChart using Interaction Trees. CoRR Kangfeng Ye, Simon Foster, Jim Woodcock
2023	J	`jnl`	How do we engineer trustworthy digital twins? Res. Dir. Cyber Phys. Syst. Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock
2023	J	`jnl`	How to ensure safety of learning-enabled cyber-physical systems? Res. Dir. Cyber Phys. Syst. Nicola Paoletti, Jim Woodcock
2023	J	`jnl`	Introduction to the Special Section on Reliability, Safety, and Security of Railway Systems. Formal Aspects Comput. Simon Collart Dutilleul, Anne E. Haxthausen, Thierry Lecomte, Jim Woodcock
2023	C	`conf`	Modelling and Verifying Robotic Software that Uses Neural Networks. ICTAC Ziggy Attala, Ana Cavalcanti, Jim Woodcock
2023	—	`conf`	Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment. CASE Mustafa Adam, Kangfeng Ye, David A. Anisi, Ana Cavalcanti, Jim Woodcock, Robert Morris
2023	J	`jnl`	Probabilistic relations for modelling epistemic and aleatoric uncertainty: its semantics and automated reasoning with theorem proving. CoRR Kangfeng Ye, Jim Woodcock, Simon Foster
2023	J	`jnl`	State of the Art Report: Verified Computation. CoRR Jim Woodcock, Mikkel Schmidt 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
2023	J	`jnl`	Time-Sensitive Software. Res. Dir. Cyber Phys. Syst. Edward A. Lee, Jim Woodcock
2023	—	`conf`	Towards a Unifying Framework for Uncertainty in Cyber-Physical Systems. Applicable Formal Methods for Safe Industrial Products Jim Woodcock
2023	J	`jnl`	Trustworthy Autonomous Systems Through Verifiability. Computer Mohammad Reza Mousavi, Ana Cavalcanti, Michael Fisher, Louise A. Dennis, Robert M. Hierons, Bilal Y. Kaddouh, Effie Lai-Chong Law, Rob Richardson, Jan Oliver Ringert, Ivan Tyukin, Jim Woodcock
2023	—	`conf`	UTP, Circus, and Isabelle. Theories of Programming and Formal Methods Jim Woodcock, Ana Cavalcanti, Simon Foster, Marcel Oliveira, Augusto Sampaio, Frank Zeyda
2023	J	`jnl`	What are the fundamental software abstractions for designing reliable cyber-physical systems operating in uncertain environments? Res. Dir. Cyber Phys. Syst. David Broman, Jim Woodcock
2022	J	`jnl`	A Pattern-based deadlock-freedom analysis strategy for concurrent systems. CoRR Pedro Antonino, Augusto Sampaio, Jim Woodcock
2022	J	`jnl`	A Survey of Practical Formal Methods for Security. Formal Aspects Comput. Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter W. V. Tran-Jørgensen, Jim Woodcock
2022	—	`conf`	Engineering of Digital Twins for Cyber-Physical Systems. ISoLA (4) John S. Fitzgerald, Peter Gorm Larsen, Tiziana Margaria, Jim Woodcock, Cláudio Gomes
2022	C	`conf`	Formally Verified Animation for RoboChart Using Interaction Trees. ICFEM Kangfeng Ye, Simon Foster, Jim Woodcock
2022	—	`conf`	Formally Verified Self-adaptation of an Incubator Digital Twin. ISoLA (4) Thomas Wright, Cláudio Gomes, Jim Woodcock
2022	J	`jnl`	Probabilistic modelling and verification using RoboChart and PRISM. Softw. Syst. Model. Kangfeng Ye, Ana Cavalcanti, Simon Foster, Alvaro Miyazawa, Jim Woodcock
2021	J	`jnl`	A Manifesto for Applicable Formal Methods. CoRR Mario Gleirscher, Jaco van de Pol, Jim Woodcock
2021	J	`jnl`	A Survey of Practical Formal Methods for Security. CoRR Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter Würtz Vinther Tran-Jørgensen, Jim Woodcock
2021	C	`conf`	Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving. RAMiCS Kangfeng Ye, Simon Foster, Jim Woodcock
2021	J	`jnl`	Automated verification of reactive and concurrent programs by calculation. J. Log. Algebraic Methods Program. Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock
2021	Misc	`ed.`	Dependable Software Engineering. Theories, Tools, and Applications - 7th International Symposium, SETTA 2021, Beijing, China, November 25-27, 2021, Proceedings SETTA Shengchao Qin, Jim Woodcock, Wenhui Zhang
2021	J	`jnl`	Editorial. Formal Aspects Comput. Xiaoping Chen, Zhiming Liu, Ji Wang, Jim Woodcock
2021	J	`jnl`	Editorial. Formal Aspects Comput. Alessandro Fantechi, Anne E. Haxthausen, Jim Woodcock
2021	B	`conf`	Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL. CONCUR Simon Foster, Chung-Kil Hur, Jim Woodcock
2021	J	`jnl`	Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL. CoRR Simon Foster, Chung-Kil Hur, Jim Woodcock
2021	—	`ch.`	Hoare and He's Unifying Theories of Programming. Theories of Programming Jim Woodcock
2021	J	`jnl`	Learning safe neural network controllers with barrier certificates. Formal Aspects Comput. Hengjun Zhao, Xia Zeng, Taolue Chen, Zhiming Liu, Jim Woodcock
2021	—	`ed.`	Proceedings First Workshop on Applicable Formal Methods, AppFM@FM 2021, virtual, 23rd November 2021. AppFM@FM Mario Gleirscher, Jaco van de Pol, Jim Woodcock
2021	J	`jnl`	RiskStructures: A design algebra for risk-aware machines. Formal Aspects Comput. Mario Gleirscher, Radu Calinescu, Jim Woodcock
2021	—	`conf`	Verification and Uncertainties in Self-integrating System. ACSOS-C Lukas Esterle, Barry Porter, Jim Woodcock
2021	—	`ch.`	Verification in the Grand Challenge. Theories of Programming Jim Woodcock, Janet Barnes, Rod Chapman, Simon Foster, Thomas Santen
2021	C	`conf`	Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps. FMICS Simon Thrane Hansen, Cláudio Gomes, Maurizio Palmieri, Casper Thule, Jaco van de Pol, Jim Woodcock
2020	J	`jnl`	Automated Verification of Reactive and Concurrent Programs by Calculation. CoRR Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock
2020	J	`jnl`	Development Automation of Real-Time Java: Model-Driven Transformation and Synthesis. ACM Trans. Embed. Comput. Syst. Wanli Chang, Ran Wei, Shuai Zhao, Andy J. Wellings, Jim Woodcock, Alan Burns
2020	—	`conf`	Engineering of Digital Twins for Cyber-Physical Systems. ISoLA (4) John S. Fitzgerald, Peter Gorm Larsen, Tiziana Margaria, Jim Woodcock
2020	Misc	`conf`	Learning Safe Neural Network Controllers with Barrier Certificates. SETTA Hengjun Zhao, Xia Zeng, Taolue Chen, Zhiming Liu, Jim Woodcock
2020	J	`jnl`	Learning Safe Neural Network Controllers with Barrier Certificates. CoRR Hengjun Zhao, Xia Zeng, Taolue Chen, Zhiming Liu, Jim Woodcock
2020	J	`jnl`	New Opportunities for Integrated Formal Methods. ACM Comput. Surv. Mario Gleirscher, Simon Foster, Jim Woodcock
2020	—	`conf`	Uncertainty Quantification and Runtime Monitoring Using Environment-Aware Digital Twins. ISoLA (4) Jim Woodcock, Cláudio Gomes, Hugo Daniel Macedo, Peter Gorm Larsen
2020	J	`jnl`	Unifying semantic foundations for automated verification tools in Isabelle/UTP. Sci. Comput. Program. Simon Foster, James Baxter, Ana Cavalcanti, Jim Woodcock, Frank Zeyda
2020	J	`jnl`	Unifying theories of reactive design contracts. Theor. Comput. Sci. Simon Foster, Ana Cavalcanti, Samuel Canham, Jim Woodcock, Frank Zeyda
2019	—	`conf`	A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic. UTP Tony Hoare, Georg Struth, Jim Woodcock
2019	—	`conf`	Probabilistic Semantics for RoboChart - A Weakest Completion Approach. UTP Jim Woodcock, Ana Cavalcanti, Simon Foster, Alexandre Mota, Kangfeng Ye
2019	J	`jnl`	RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. Alvaro Miyazawa, Pedro Ribeiro, Wei Li, Ana Cavalcanti, Jon Timmis, Jim Woodcock
2019	J	`jnl`	Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP. CoRR Simon Foster, James Baxter, Ana Cavalcanti, Jim Woodcock, Frank Zeyda
2018	—	`conf`	Analysing RoboChart with Probabilities. SBMF Madiel S. Conserva Filho, R. Marinho, Alexandre Mota, Jim Woodcock
2018	J	`jnl`	Assuring Autonomous Systems: Opportunities for Integrated Formal Methods? CoRR Mario Gleirscher, Simon Foster, Jim Woodcock
2018	—	`conf`	Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. FACS Simon Foster, James Baxter, Ana Cavalcanti, Alvaro Miyazawa, Jim Woodcock
2018	J	`jnl`	Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. CoRR Simon Foster, James Baxter, Ana Cavalcanti, Alvaro Miyazawa, Jim Woodcock
2018	C	`conf`	Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. RAMiCS Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock
2018	J	`jnl`	Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. CoRR Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock
2018	—	`conf`	Cyber-Physical Systems Engineering: An Introduction. ISoLA (3) J. Paul Gibson, Peter Gorm Larsen, Marc Pantel, John S. Fitzgerald, Jim Woodcock
2018	J	`jnl`	Unifying theories of time with generalised reactive processes. Inf. Process. Lett. Simon Foster, Ana Cavalcanti, Jim Woodcock, Frank Zeyda
2017	J	`jnl`	Editorial. Formal Aspects Comput. Maurizio Proietti, Hirohisa Seki, Jim Woodcock
2017	—	`conf`	Features of Integrated Model-Based Co-modelling and Co-simulation Technology. SEFM Workshops Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock, Carl Gamble, Richard John Payne, Kenneth Pierce
2017	J	`jnl`	From Formalised State Machines to Implementations of Robotic Controllers. CoRR Wei Li, Alvaro Miyazawa, Pedro Ribeiro, Ana Cavalcanti, Jim Woodcock, Jon Timmis
2017	J	`jnl`	Model checking of state-rich formalism Int. J. Softw. Tools Technol. Transf. Kangfeng Ye, Jim Woodcock
2017	—	`ch.`	Sound Simulation and Co-simulation for Robotics. Present and Ulterior Software Engineering Ana Cavalcanti, Alvaro Miyazawa, Richard John Payne, Jim Woodcock
2017	—	`conf`	Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL. Concurrency, Security, and Puzzles Simon Foster, Jim Woodcock
2017	J	`jnl`	Unifying Theories of Reactive Design Contracts. CoRR Simon Foster, Ana Cavalcanti, Samuel Canham, Jim Woodcock, Frank Zeyda
2017	J	`jnl`	Unifying Theories of Timed with Generalised Reactive Processes. CoRR Simon Foster, Ana Cavalcanti, Jim Woodcock, Frank Zeyda
2017	J	`jnl`	What can agile methods bring to high-integrity software development? Commun. ACM Roderick Chapman, Neil White, Jim Woodcock
2016	—	`conf`	A Stepwise Approach to Linking Theories. UTP Pedro Ribeiro, Ana Cavalcanti, Jim Woodcock
2016	C	`conf`	Behavioural Models for FMI Co-simulations. ICTAC Ana Cavalcanti, Jim Woodcock, Nuno Amálio
2016	C	`conf`	Checking SysML Models for Co-simulation. ICFEM Nuno Amálio, Richard John Payne, Ana Cavalcanti, Jim Woodcock
2016	—	`conf`	From Formalised State Machines to Implementations of Robotic Controllers. DARS Wei Li, Alvaro Miyazawa, Pedro Ribeiro, Ana Cavalcanti, Jim Woodcock, Jon Timmis
2016	—	`conf`	Heterogeneous Semantics and Unifying Theories. ISoLA (1) Jim Woodcock, Simon Foster, Andrew Butterfield
2016	—	`conf`	Integrated tool chain for model-based design of Cyber-Physical Systems: The INTO-CPS project. CPS Data 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
2016	—	`conf`	Java in the Safety-Critical Domain. SETSS Ana Cavalcanti, Alvaro Miyazawa, Andy J. Wellings, Jim Woodcock, Shuai Zhao
2016	—	`conf`	Towards Semantically Integrated Models and Tools for Cyber-Physical Systems Design. ISoLA (2) Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock, René A. Nilsson, Carl Gamble, Simon Foster
2016	—	`conf`	Towards a UTP Semantics for Modelica. UTP Simon Foster, Bernhard Thiele, Ana Cavalcanti, Jim Woodcock
2016	—	`conf`	UTP Semantics of Reactive Processes with Continuations. UTP Gerard Ekembe Ngondi, Jim Woodcock
2016	—	`conf`	UTP by Example: Designs. SETSS Jim Woodcock, Simon Foster
2016	C	`conf`	Unifying Heterogeneous State-Spaces with Lenses. ICTAC Simon Foster, Frank Zeyda, Jim Woodcock
2015	C	`conf`	CSP and Kripke Structures. ICTAC Ana Cavalcanti, Wen-ling Huang, Jan Peleska, Jim Woodcock
2015	—	`conf`	Cyber-Physical Systems Design: Formal Foundations, Methods and Integrated Tool Chains. FormaliSE@ICSE John S. Fitzgerald, Carl Gamble, Peter Gorm Larsen, Kenneth Pierce, Jim Woodcock
2015	J	`jnl`	Editorial. Formal Aspects Comput. Jim Woodcock, Cliff B. Jones
2015	—	`ch.`	Mechanised Theory Engineering in Isabelle. Dependable Software Systems Engineering Simon Foster, Jim Woodcock
2015	—	`conf`	Mobile CSP. SBMF Jim Woodcock, Andy J. Wellings, Ana Cavalcanti
2015	J	`jnl`	Model checking CML: tool development and industrial applications. Formal Aspects Comput. Alexandre Mota, Adalberto Farias, Jim Woodcock, Peter Gorm Larsen
2015	C	`conf`	Refinement-Based Verification of the FreeRTOS Scheduler in VCC. ICFEM Sumesh Divakaran, Deepak D'Souza, Anirudh Kushwah, Prahladavaradan Sampath, Nigamanth Sridhar, Jim Woodcock
2015	J	`jnl`	Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions. ACM Comput. Surv. Claus Ballegaard Nielsen, Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock, Jan Peleska
2015	J	`jnl`	Using formal reasoning on a model of tasks for FreeRTOS. Formal Aspects Comput. Shu Cheng, Jim Woodcock, Deepak D'Souza
2014	B	`conf`	A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes. FM Pedro R. G. Antonino, Augusto Sampaio, Jim Woodcock
2014	J	`jnl`	Adapting FreeRTOS for multicores: an experience report. Softw. Pract. Exp. James Mistry, Matthew Naylor, Jim Woodcock
2014	—	`conf`	An approach for managing semantic heterogeneity in Systems of Systems Engineering. SoSE Simon Foster, Alvaro Miyazawa, Jim Woodcock, Ana Cavalcanti, John S. Fitzgerald, Peter Gorm Larsen
2014	—	`conf`	Contracts in CML. ISoLA (2) Jim Woodcock, Ana Cavalcanti, John S. Fitzgerald, Simon Foster, Peter Gorm Larsen
2014	B	`conf`	Engineering UToPiA - Formal Semantics for CML. FM Jim Woodcock
2014	—	`conf`	Isabelle/UTP: A Mechanised Theory Engineering Framework. UTP Simon Foster, Frank Zeyda, Jim Woodcock
2014	B	`conf`	Rapid Prototyping of a Semantically Well Founded Circus Model Checker. SEFM Alexandre Mota, Adalberto Farias, André Didier, Jim Woodcock
2014	J	`jnl`	Test-data generation for control coverage by proof. Formal Aspects Comput. Ana Cavalcanti, Steve King, Colin O'Halloran, Jim Woodcock
2014	—	`conf`	Three Approaches to Timed External Choice in UTP. UTP Samuel Canham, Jim Woodcock
2014	—	`conf`	Towards Algebraic Semantics of Circus Time. UTP Kun Wei, Jim Woodcock
2013	B	`conf`	A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP. SEFM Marcel Vinícius Medeiros Oliveira, Ivan Soares de Medeiros Júnior, Jim Woodcock
2013	—	`conf`	Foundations for Model-Based Engineering of Systems of Systems. CSDM John S. Fitzgerald, Peter Gorm Larsen, Jim Woodcock
2013	—	`ch.`	Industrial Deployment of Formal Methods: Trends and Challenges. Industrial Deployment of System Engineering Methods John S. Fitzgerald, Juan Bicarregui, Peter Gorm Larsen, Jim Woodcock
2013	J	`jnl`	Modelling temporal behaviour in complex systems with Timebands. Formal Methods Syst. Des. Kun Wei, Jim Woodcock, Alan Burns
2013	J	`jnl`	Safety-critical Java programs from Circus models. Real Time Syst. Ana Cavalcanti, Frank Zeyda, Andy J. Wellings, Jim Woodcock, Kun Wei
2013	—	`conf`	Simulink Timed Models for Program Verification. Theories of Programming and Formal Methods Ana Cavalcanti, Alexandre Mota, Jim Woodcock
2013	J	`jnl`	The Safety-Critical Java memory model formalised. Formal Aspects Comput. Ana Cavalcanti, Andy J. Wellings, Jim Woodcock
2013	C	`ed.`	Theoretical Aspects of Computing - ICTAC 2013 - 10th International Colloquium, Shanghai, China, September 4-6, 2013. Proceedings ICTAC Zhiming Liu, Jim Woodcock, Huibiao Zhu
2013	—	`ed.`	Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday Theories of Programming and Formal Methods Zhiming Liu, Jim Woodcock, Huibiao Zhu
2013	—	`conf`	Unifying Theories of Logic and Specification. SBMF Victor Bandur, Jim Woodcock
2013	—	`ed.`	Unifying Theories of Programming and Formal Engineering Methods - International Training School on Software Engineering, Held at ICTAC 2013, Shanghai, China, August 26-30, 2013, Advanced Lectures ICTAC Training School on Software Engineering Zhiming Liu, Jim Woodcock, Huibiao Zhu
2013	—	`conf`	Unifying Theories of Programming in Isabelle. ICTAC Training School on Software Engineering Simon Foster, Jim Woodcock
2013	J	`jnl`	Unifying theories in ProofPower-Z. Formal Aspects Comput. Marcel Oliveira, Ana Cavalcanti, Jim Woodcock
2012	B	`conf`	A Plug-in Based Approach for UML Model Simulation. ECMFA Alek Radjenovic, Richard F. Paige, Louis M. Rose, Jim Woodcock, Steve King
2012	J	`jnl`	Editorial. Formal Aspects Comput. Jim Woodcock
2012	—	`conf`	Features of CML: A formal modelling language for Systems of Systems. SoSE Jim Woodcock, Ana Cavalcanti, John S. Fitzgerald, Peter Gorm Larsen, Alvaro Miyazawa, Simon Perry
2012	J	`jnl`	Mechanised wire-wise verification of Handel-C synthesis. Sci. Comput. Program. Juan Ignacio Perna, Jim Woodcock
2012	—	`ch.`	Modelling Temporal Behaviour in Complex Systems with Timebands. Conquering Complexity Kun Wei, Jim Woodcock, Alan Burns
2012	—	`conf`	Unifying Theories of Undefinedness in UTP. UTP Jim Woodcock, Victor Bandur
2011	J	`jnl`	Correct hardware synthesis - An algebraic approach. Acta Informatica Juan Ignacio Perna, Jim Woodcock, Augusto Sampaio, Juliano Iyoda
2011	J	`jnl`	Editorial. Formal Aspects Comput. Daniel Kroening, Tiziana Margaria, Jim Woodcock
2011	J	`jnl`	Editorial. Formal Aspects Comput. Zhiming Liu, Jim Woodcock
2011	—	`conf`	Safety-critical Java in Circus. JTRES Ana Cavalcanti, Andy J. Wellings, Jim Woodcock, Kun Wei, Frank Zeyda
2011	B	`conf`	The Safety-Critical Java Memory Model: A Formal Account. FM Ana Cavalcanti, Andy J. Wellings, Jim Woodcock
2011	B	`conf`	Timed Circus: Timed CSP with the Miracle. ICECCS Kun Wei, Jim Woodcock, Alan Burns
2011	B	`conf`	Using Model Transformation to Generate Graphical Counter-Examples for the Formal Analysis of xUML Models. ICECCS Osmar Marchi dos Santos, Jim Woodcock, Richard F. Paige
2010	B	`conf`	A Timed Model of Circus with the Reactive Design Miracle. SEFM Kun Wei, Jim Woodcock, Alan Burns
2010	J	`jnl`	Considering Software Preservation. ERCIM News Brian Matthews, Arif Shaon, Juan Bicarregui, Catherine Mary Jones, Esther Conway, Jim Woodcock
2010	—	`conf`	Modelling and Implementing Complex Systems with Timebands. SSIRI Jim Woodcock, Marcel Oliveira, Alan Burns, Kun Wei
2010	—	`ch.`	Programming Phase: Formal Methods. Encyclopedia of Software Engineering Richard F. Paige, Jim Woodcock, Phillip J. Brooke, Ana Cavalcanti
2010	—	`ed.`	Testing Techniques in Software Engineering, Second Pernambuco Summer School on Software Engineering, PSSE 2007, Recife, Brazil, December 3-7, 2007, Revised Lectures PSSE Paulo Borba, Ana Cavalcanti, Augusto Sampaio, Jim Woodcock
2010	—	`ch.`	The Tokeneer Experiments. Reflections on the Work of C. A. R. Hoare Jim Woodcock, Emine Gökçe Aydal, Rod Chapman
2010	C	`ed.`	Theoretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010. Proceedings ICTAC Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel, Jim Woodcock
2009	J	`jnl`	A Chain Datatype in Z. Int. J. Softw. Informatics Leo Freitas, Jim Woodcock
2009	J	`jnl`	A UTP semantics for Formal Aspects Comput. Marcel Oliveira, Ana Cavalcanti, Jim Woodcock
2009	J	`jnl`	FDR Explorer. Formal Aspects Comput. Leo Freitas, Jim Woodcock
2009	—	`ed.`	Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers SBMF Marcel Vinícius Medeiros Oliveira, Jim Woodcock
2009	J	`jnl`	Formal methods: Practice and experience. ACM Comput. Surv. Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, John S. Fitzgerald
2009	J	`jnl`	Mechanising a formal model of flash memory. Sci. Comput. Program. Andrew Butterfield, Leo Freitas, Jim Woodcock
2009	J	`jnl`	POSIX file store in Z/Eves: An experiment in the verified software repository. Sci. Comput. Program. Leo Freitas, Jim Woodcock, Zheng Fu
2009	A	`conf`	Putting Formal Specifications under the Magnifying Glass: Model-based Testing for Validation. ICST Emine Gokce Aydal, Richard F. Paige, Mark Utting, Jim Woodcock
2009	Misc	`conf`	State Visibility and Communication in Unifying Theories of Programming. TASE Andrew Butterfield, Pawel Gancarski, Jim Woodcock
2009	—	`conf`	The Use of Model Transformation in the INESS Project. FMCO Osmar Marchi dos Santos, Jim Woodcock, Richard F. Paige, Steve King
2009	—	`conf`	Towards a Methodology for Software Preservation. iPRES Brian Matthews, Esther Conway, Jim Woodcock, Catherine Mary Jones, Juan Bicarregui, Arif Shaon
2009	J	`jnl`	Verifying the CICS File Control API with Z/Eves: An experiment in the verified software repository. Sci. Comput. Program. Leo Freitas, Jim Woodcock, Yichi Zhang
2008	—	`conf`	A Comparison of State-Based Modelling Tools for Model Validation. TOOLS (46) Emine Gokce Aydal, Mark Utting, Jim Woodcock
2008	C	`conf`	A Theory of Pointers for the UTP. ICTAC Will Harwood, Ana Cavalcanti, Jim Woodcock
2008	C	`conf`	ABZ2008 VSR-Net Workshop. ABZ Jim Woodcock, Paul Boca
2008	J	`jnl`	Editorial. Formal Aspects Comput. Cliff B. Jones, Jim Woodcock
2008	J	`jnl`	Evaluation of OCL for Large-Scale Modelling: A Different View of the Mondex Purse. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Emine Gokce Aydal, Richard F. Paige, Jim Woodcock
2008	B	`conf`	Linking VDM and Z. ICECCS Jim Woodcock, Leo Freitas
2008	—	`conf`	Mechanised Wire-wise Verification of Handel-C Synthesis. SBMF Juan Ignacio Perna, Jim Woodcock
2008	J	`jnl`	Mechanising Mondex with Z/Eves. Formal Aspects Comput. Leo Freitas, Jim Woodcock
2008	—	`conf`	Observations for Assertion-based Scenarios in the context of Model Validation and Extension to Test Case Generation. ICST Workshops Emine Gokce Aydal, Richard F. Paige, Jim Woodcock
2008	B	`conf`	POSIX and the Verification Grand Challenge: A Roadmap. ICECCS Leo Freitas, Jim Woodcock, Andrew Butterfield
2008	—	`conf`	The Miracle of Reactive Programming. UTP Jim Woodcock
2008	J	`jnl`	The certification of the Mondex electronic purse to ITSEC Level E6. Formal Aspects Comput. Jim Woodcock, Susan Stepney, David Cooper, John A. Clark, Jeremy Jacob
2008	—	`conf`	UTP Semantics for Handel-C. UTP Juan Ignacio Perna, Jim Woodcock
2008	—	`conf`	Unifying Theories of Interrupts. UTP Alistair A. McEwan, Jim Woodcock
2008	—	`ed.`	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 Bertrand Meyer, Jim Woodcock
2008	—	`ed.`	Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings VSTTE Natarajan Shankar, Jim Woodcock
2007	C	`conf`	A Denotational Semantics for Handel-C Hardware Compilation. ICFEM Juan Ignacio Perna, Jim Woodcock
2007	C	`conf`	Automatic Generation of Verified Concurrent Hardware. ICFEM Marcel Oliveira, Jim Woodcock
2007	—	`ed.`	Domain Modeling and the Duration Calculus, International Training School, Shanghai, China, September 17-21. 2007, Advanced Lectures Domain Modeling and the Duration Calculus Chris George, Zhiming Liu, Jim Woodcock
2007	J	`jnl`	Editorial. Formal Aspects Comput. Cliff B. Jones, Jim Woodcock
2007	—	`conf`	Evaluation of OCL for Large-Scale Modelling: A Different View of the Mondex Purse. MoDELS (Workshops) Emine Gokce Aydal, Richard F. Paige, Jim Woodcock
2007	—	`ed.`	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 Cliff B. Jones, Zhiming Liu, Jim Woodcock
2007	B	`conf`	Formalising Flash Memory: First Steps. ICECCS Andrew Butterfield, Jim Woodcock
2007	—	`conf`	Goal-Oriented Automatic Test Case Generators for MC/DC Compliancy. ICSOFT (SE) Emine Gokce Aydal, Jim Woodcock, Ana Cavalcanti
2007	B	`conf`	POSIX file store in Z/Eves: an experiment in the verified software repository. ICECCS Leo Freitas, Zheng Fu, Jim Woodcock
2007	—	`conf`	Proving Theorems About JML Classes. Formal Methods and Hybrid Real-Time Systems Leo Freitas, Jim Woodcock
2007	B	`conf`	Slotted-Circus. IFM Andrew Butterfield, Adnan Sherif, Jim Woodcock
2007	J	`jnl`	The Verification Grand Challenge. J. Univers. Comput. Sci. Jim Woodcock, Richard Banach
2007	C	`ed.`	Theoretical Aspects of Computing - ICTAC 2007, 4th International Colloquium, Macau, China, September 26-28, 2007, Proceedings ICTAC Cliff B. Jones, Zhiming Liu, Jim Woodcock
2007	B	`conf`	Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository. ICECCS Leo Freitas, Konstantinos Mokos, Jim Woodcock
2006	—	`conf`	A Denotational Semantics for Circus. Refine@ICFEM Marcel Oliveira, Ana Cavalcanti, Jim Woodcock
2006	B	`conf`	A Layered Behavioural Model of Platelets. ICECCS Steve A. Schneider, Helen Treharne, Ana Cavalcanti, Jim Woodcock
2006	—	`conf`	An Operational Semantics in UTP for a Language of Reactive Designs (Abstract). UTP Jim Woodcock
2006	J	`jnl`	Angelic nondeterminism in the unifying theories of programming. Formal Aspects Comput. Ana Cavalcanti, Jim Woodcock, Steve Dunne
2006	—	`conf`	FDR Explorer. Refine@ICFEM Leo Freitas, Jim Woodcock
2006	C	`conf`	First Steps in the Verified Software Grand Challenge. SEW Jim Woodcock
2006	J	`jnl`	First Steps in the Verified Software Grand Challenge. Computer Jim Woodcock
2006	—	`conf`	Mechanising a Unifying Theory. UTP Gift Nuka, Jim Woodcock
2006	—	`conf`	Pointers and Records in the Unifying Theories of Programming. UTP Ana Cavalcanti, Will Harwood, Jim Woodcock
2006	—	`ed.`	Refinement Techniques in Software Engineering, First Pernambuco Summer School on Software Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004, Revised Lectures PSSE Ana Cavalcanti, Augusto Sampaio, Jim Woodcock
2006	J	`jnl`	State-rich model checking. Innov. Syst. Softw. Eng. Leo Freitas, Jim Woodcock, Ana Cavalcanti
2006	C	`conf`	Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking. ICFEM Leo Freitas, Ana Cavalcanti, Jim Woodcock
2006	—	`conf`	Unifying Theories in ProofPower-Z. UTP Marcel Oliveira, Ana Cavalcanti, Jim Woodcock
2006	B	`conf`	Verified Software Grand Challenge. FM Jim Woodcock
2006	J	`jnl`	Verified Software: A Grand Challenge. Computer Cliff B. Jones, Peter W. O'Hearn, Jim Woodcock
2006	C	`conf`	Z/Eves and the Mondex Electronic Purse. ICTAC Jim Woodcock, Leo Freitas
2005	—	`conf`	Angelic Nondeterminism and Unifying Theories of Programming. REFINE Ana Cavalcanti, Jim Woodcock
2005	J	`jnl`	Formal development of industrial-scale systems in Innov. Syst. Softw. Eng. Marcel Oliveira, Ana Cavalcanti, Jim Woodcock
2005	B	`conf`	Operational Semantics for Model Checking Circus. FM Jim Woodcock, Ana Cavalcanti, Leonardo Freitas
2005	—	`conf`	Simpler Reasoning About System Properties: a Proof-by-Refinement Technique. REFINE Diyaa-Addein Atiya, Steve King, Jim Woodcock
2005	—	`conf`	Unifying Program Refinement Calculi. Abstract State Machines Jim Woodcock
2005	J	`jnl`	Unifying classes and processes. Softw. Syst. Model. Ana Cavalcanti, Augusto Sampaio, Jim Woodcock
2005	J	`jnl`	prialt in Handel-C: an operational semantics. Int. J. Softw. Tools Technol. Transf. Andrew Butterfield, Jim Woodcock
2004	—	`conf`	A "Hardware Compiler" Semantics for Handel-C. MFCSIT Andrew Butterfield, Jim Woodcock
2004	—	`conf`	A Tutorial Introduction to CSP in PSSE Ana Cavalcanti, Jim Woodcock
2004	B	`conf`	A Tutorial Introduction to Designs in Unifying Theories of Programming. IFM Jim Woodcock, Ana Cavalcanti
2004	—	`conf`	Refinement: An overview. PSSE Ana Cavalcanti, Augusto Sampaio, Jim Woodcock
2004	B	`conf`	Towards Mobile Processes in Unifying Theories. SEFM Xinbei Tang, Jim Woodcock
2004	B	`conf`	Travelling Processes. MPC Xinbei Tang, Jim Woodcock
2003	—	`conf`	A Circus Semantics for Ravenscar Protected Objects. FME Diyaa-Addein Atiya, Steve King, Jim Woodcock
2003	J	`jnl`	A Refinement Strategy for Circus. Formal Aspects Comput. Ana Cavalcanti, Augusto Sampaio, Jim Woodcock
2003	C	`conf`	An Operational Semantics for Handel-C. FMICS Andrew Butterfield, Jim Woodcock
2003	J	`jnl`	ArcAngel: a Tactic Language for Refinement. Formal Aspects Comput. Marcel Oliveira, Ana Cavalcanti, Jim Woodcock
2003	C	`ed.`	Formal Methods and Software Engineering, 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003, Proceedings ICFEM Jin Song Dong, Jim Woodcock
2003	—	`conf`	Mechanising the Alphabetised Relational Calculus. WMF Gift Nuka, Jim Woodcock
2003	J	`jnl`	Predicate transformers in the semantics of Circus. IEE Proc. Softw. Ana Cavalcanti, Jim Woodcock
2003	—	`conf`	Using Circus for Safety-critical Applications. WMF Jim Woodcock
2002	—	`ed.`	BCS FACS Refinement Workshop 2002, Refine 2002, Satellite Event of FLoC 2002, Copenhagen, Denmark, July 20-21, 2002 Refine John Derrick, Eerke A. Boiten, Jim Woodcock, Joakim von Wright
2002	—	`conf`	Preface. Refine John Derrick, Eerke A. Boiten, Jim Woodcock, Joakim von Wright
2002	—	`conf`	Refinement in Circus. FME Augusto Sampaio, Jim Woodcock, Ana Cavalcanti
2002	—	`conf`	Refinement of actions in Circus. Refine Ana Cavalcanti, Augusto Sampaio, Jim Woodcock
2002	—	`conf`	Semantic domains for Handel-C. MFCSIT Andrew Butterfield, Jim Woodcock
2002	—	`conf`	The Semantics of Circus. ZB Jim Woodcock, Ana Cavalcanti
2002	C	`conf`	Unifying Theories of Parallel Programming. ICFEM Jim Woodcock, Arthur P. Hughes
2001	—	`conf`	A Concurrent Language for Refinement. IWFM Jim Woodcock, Ana Cavalcanti
2001	C	`conf`	The Steam Boiler in a Unified Theory of Z and CSP. APSEC Jim Woodcock, Ana Cavalcanti
2000	J	`jnl`	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. Jeannette M. Wing, Jim Woodcock
2000	J	`jnl`	Introduction: Special Issues for FM'99, the First World Congress on Formal Methods in the Development of Computing Systems. Formal Methods Syst. Des. Jeannette M. Wing, Jim Woodcock
2000	J	`jnl`	The First World Congress on Formal Methods in the Development of Computing Systems. Formal Aspects Comput. Jeannette M. Wing, Jim Woodcock
1999	J	`jnl`	An Inconsistency in Procedures, Parameters, and Substitution in the Refinement Calculus. Sci. Comput. Program. Ana Cavalcanti, Augusto Sampaio, Jim Woodcock
1999	—	`ed.`	FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume I World Congress on Formal Methods Jeannette M. Wing, Jim Woodcock, Jim Davies
1999	—	`ed.`	FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume II World Congress on Formal Methods Jeannette M. Wing, Jim Woodcock, Jim Davies
1999	B	`conf`	On the Refinement and Simulation of Data Types and Processes. IFM Christie Bolton, Jim Davies, Jim Woodcock
1999	—	`conf`	When to Trust Mobile Objects: Access Control in the Jini(tm) Software System. TOOLS (30) Charles Crichton, Jim Davies, Jim Woodcock
1998	J	`jnl`	A Weakest Precondition Semantics for Z. Comput. J. Ana Cavalcanti, Jim Woodcock
1998	—	`conf`	More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement. ZUM Susan Stepney, David Cooper, Jim Woodcock
1998	J	`jnl`	Procedures and Recursion in the Refinement Calculus. J. Braz. Comput. Soc. Ana Cavalcanti, Augusto Sampaio, Jim Woodcock
1998	—	`conf`	Safety through Security. IWSSD Andrew Simpson, Jim Woodcock, Jim Davies
1998	J	`jnl`	ZRC - A Refinement Calculus for Z. Formal Aspects Comput. Ana Cavalcanti, Jim Woodcock
1996	J	`jnl`	A Tactic Calculus-Abridged Version. Formal Aspects Comput. Andrew P. Martin, Paul H. B. Gardiner, Jim Woodcock
1996	—	`ed.`	FME '96: Industrial Benefit and Advances in Formal Methods, Third International Symposium of Formal Methods Europe, Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18-22, 1996, Proceedings FME Marie-Claude Gaudel, Jim Woodcock
1996	J	`jnl`	Non-interference through Determinism. J. Comput. Secur. A. W. Roscoe, Jim Woodcock, Lars Wulf
1996	J	`jnl`	Software Engineering Research Directions. ACM Comput. Surv. Jim Woodcock
1995	J	`jnl`	Event Refinement in State-Based Concurrent Systems. Formal Aspects Comput. Jane E. Sinclair, Jim Woodcock
1995	J	`jnl`	Introduction to Special Section (Guest Editorial). IEEE Trans. Software Eng. Jim Woodcock, Peter Gorm Larsen
1994	A	`conf`	Non-Interference Through Determinism. ESORICS A. W. Roscoe, Jim Woodcock, Lars Wulf
1994	—	`conf`	The Formal Specification in Z of Defence Standard 00-56. Z User Workshop Jim Woodcock, Paul H. B. Gardiner, J. R. Hulance
1993	—	`ed.`	FME '93: Industrial-Strength Formal Methods, First International Symposium of Formal Methods Europe, Odense, Denmark, April 19-23, 1993, Proceedings FME Jim Woodcock, Peter Gorm Larsen
1993	B	`ed.`	Mathematics of Program Construction, Second International Conference, Oxford, UK, June 29 - July 3, 1992, Proceedings MPC Richard S. Bird, Carroll Morgan, Jim Woodcock
1992	J	`jnl`	The Rudiments of Algorithm Refinement. Comput. J. Jim Woodcock
1991	—	`conf`	A Tutorial on the Refinement Calculus. VDM Europe (2) Jim Woodcock
1991	—	`conf`	An Introduction to Refinement in Z. VDM Europe (2) Jim Woodcock
1991	—	`conf`	The Refinement Calculus. VDM Europe (2) Jim Woodcock
1991	—	`conf`	Two Refinement Case Studies. VDM Europe (2) Jim Woodcock
1990	—	`conf`	A Simpler Semantics for Z. Z User Workshop Paul H. B. Gardiner, P. J. Lupton, Jim Woodcock
1990	—	`conf`	Refinement of State-Based Concurrent Systems. VDM Europe Jim Woodcock, Carroll Morgan
1988	—	`conf`	Using VDM with Rely and Guarantee-Conditions - Experiences from a Real Project. VDM Europe Jim Woodcock, B. Dickinson
1987	J	`jnl`	Towards the formal specification of a simple programming support environment. Softw. Eng. J. Bernard Sufrin, Jim Woodcock