Ein modellbasierter Ansatz zur Dialogsteuerung in Benutzungsoberflächen. - Friedrich Strauß; Stefan Hügel; Kirsten Winter; Britta Schinzel (Software-Ergonomie, 1995)

Model Checking for Abstract State Machines. - Kirsten Winter (J. Univers. Comput. Sci., 1997)

An Agenda for Specifying Software Components with Complex Data Models. - Kirsten Winter; Thomas Santen; Maritta Heisel (SAFECOMP, 1998)

Towards a Methodology for Model Checking ASM: Lessons Learned from the FLASH Case Study. - Kirsten Winter (Abstract State Machines, 2000)

Model Checking Support for the ASM High-Level Language. - Giuseppe Del Castillo; Kirsten Winter (TACAS, 2000)

Model checking with abstract types. - Kirsten Winter (Workshop on Software Model Checking @ CAV, 2001)

Model checking abstract state machines. - Kirsten Winter (2001)

Model Checking Railway Interlocking Systems. - Kirsten Winter (ACSC, 2002)

Model Checking Object-Z Using ASM. - Kirsten Winter; Roger Duke (IFM, 2002)

Modelling Large Railway Interlockings and Model Checking Small Ones. - Kirsten Winter; Neil J. Robinson (ACSC, 2003)

Interfacing ASM with the MDG Tool. - Amjad Gawanmeh; Sofiène Tahar; Kirsten Winter (Abstract State Machines, 2003)

Formal Verification of ASM Designs Using the MDG Tool. - Amjad Gawanmeh; Sofiène Tahar; Kirsten Winter (SEFM, 2003)

Proving Temporal Properties of Z Specifications Using Abstraction. - Graeme Smith 001; Kirsten Winter (ZB, 2003)

Compositional Verification for Object-Z. - Kirsten Winter; Graeme Smith 001 (ZB, 2003)

Formalising Behaviour Trees with CSP. - Kirsten Winter (IFM, 2004)

An Environment for Building a System out of its Requirements. - Cameron Smith; Kirsten Winter; Ian J. Hayes; R. Geoff Dromey; Peter A. Lindsay; David A. Carrington (ASE, 2004)

An Automated Failure Mode and Effect Analysis Based on High-Level Design Specification with Behavior Trees. - Lars Grunske; Peter A. Lindsay; Nisansala Yatapanage; Kirsten Winter (IFM, 2005)

Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking. - Wendy Johnston; Kirsten Winter; Lionel van den Berg; Paul A. Strooper; Peter J. Robinson 001 (FM, 2006)

Simulation Machines for Checking Action System Refinements. - Graeme Smith 001; Kirsten Winter (Refine@ICFEM, 2006)

Early Validation and Verification of a Distributed Role-Based Access Control Model. - Saad Zafar; Robert Colvin; Kirsten Winter; Nisansala Yatapanage; R. Geoff Dromey (APSEC, 2007)

Timed Behavior Trees and Their Application to Verifying Real-Time Systems. - Lars Grunske; Kirsten Winter; Robert Colvin (ASWEC, 2007)

Introducing Time in an Industrial Application of Model-Checking. - Lionel van den Berg; Paul A. Strooper; Kirsten Winter (FMICS, 2007)

Probabilistic Timed Behavior Trees. - Robert Colvin; Lars Grunske; Kirsten Winter (IFM, 2007)

Probabilistic Model-Checking Support for FMEA. - Lars Grunske; Robert Colvin; Kirsten Winter (QEST, 2007)

Formal verification of ASMs using MDGs. - Amjad Gawanmeh; Sofiène Tahar; Kirsten Winter (J. Syst. Archit., 2008)

Timed Behavior Trees for Failure Mode and Effects Analysis of time-critical systems. - Robert Colvin; Lars Grunske; Kirsten Winter (J. Syst. Softw., 2008)

Defining the abstract syntax of visual languages with advanced graph grammars - A case study based on behavior trees. - Lars Grunske; Kirsten Winter; Nisansala Yatapanage (J. Vis. Lang. Comput., 2008)

Dynamic Relational Behaviour for Large-Scale Systems. - Kirsten Winter; Robert Colvin; R. Geoff Dromey (Australian Software Engineering Conference, 2009)

Model checking action system refinements. - Graeme Smith 001; Kirsten Winter (Formal Aspects Comput., 2009)

Slicing Behavior Tree Models for Verification. - Nisansala Yatapanage; Kirsten Winter; Saad Zafar (IFIP TCS, 2010)

Safety Assessment Using Behavior Trees and Model Checking. - Peter A. Lindsay; Kirsten Winter; Nisansala Yatapanage (SEFM, 2010)

Integrating Requirements: The Behavior Tree Philosophy. - Kirsten Winter; Ian J. Hayes; Robert Colvin (SEFM, 2010)

Experience with fault injection experiments for FMEA. - Lars Grunske; Kirsten Winter; Nisansala Yatapanage; Saad Zafar; Peter A. Lindsay (Softw. Pract. Exp., 2011)

Reasoning About Adaptivity of Agents and Multi-agent Systems. - Graeme Smith 001; Jeffrey W. Sanders; Kirsten Winter (ICECCS, 2012)

Optimising Ordering Strategies for Symbolic Model Checking of Railway Interlockings. - Kirsten Winter (ISoLA (2), 2012)

Incremental Development of Multi-agent Systems in Object-Z. - Graeme Smith 001; Kirsten Winter (SEW, 2012)

Cut Set Analysis using Behavior Trees and model checking. - Peter A. Lindsay; Nisansala Yatapanage; Kirsten Winter (Formal Aspects Comput., 2012)

Path-Sensitive Data Flow Analysis Simplified. - Kirsten Winter; Chenyi Zhang 001; Ian J. Hayes; Nathan Keynes; Cristina Cifuentes; Lian Li (ICFEM, 2013)

Designing Adaptive Systems Using Teleo-Reactive Agents. - Graeme Smith 001; Jeff W. Sanders; Kirsten Winter (Trans. Comput. Collect. Intell., 2014)

Next-preserving branching bisimulation. - Nisansala Yatapanage; Kirsten Winter (Theor. Comput. Sci., 2015)

An Algebra of Synchronous Atomic Steps. - Ian J. Hayes; Robert J. Colvin; Larissa A. Meinicke; Kirsten Winter; Andrius Velykis (FM, 2016)

Relating trace refinement and linearizability. - Graeme Smith 001; Kirsten Winter (Formal Aspects Comput., 2017)

Observational Models for Linearizability Checking on Weak Memory Models. - Kirsten Winter; Graeme Smith 001; John Derrick (TASE, 2018)

A sound and complete definition of linearizability on weak memory models. - Graeme Smith 001; Kirsten Winter; Robert J. Colvin (CoRR, 2018)

Correctness of Concurrent Objects under Weak Memory Models. - Graeme Smith 001; Kirsten Winter; Robert J. Colvin (Refine@FM, 2018)

An Abstract Semantics of Speculative Execution for Reasoning About Security Vulnerabilities. - Robert J. Colvin; Kirsten Winter (FM Workshops (2), 2019)

A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. - Ian J. Hayes; Larissa A. Meinicke; Kirsten Winter; Robert J. Colvin (Formal Aspects Comput., 2019)

Modelling concurrent objects running on the TSO and ARMv8 memory models. - Kirsten Winter; Graeme Smith 001; John Derrick (Sci. Comput. Program., 2019)

Linearizability on hardware weak memory models. - Graeme Smith 001; Kirsten Winter; Robert J. Colvin (Formal Aspects Comput., 2020)

Backwards-directed information flow analysis for concurrent programs. - Kirsten Winter; Nicholas Coughlin; Graeme Smith 001 (CSF, 2021)

Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models. - Nicholas Coughlin; Kirsten Winter; Graeme Smith 001 (FM, 2021)

Compositional Reasoning for Non-multicopy Atomic Architectures. - Nicholas Coughlin; Kirsten Winter; Graeme Smith 001 (Formal Aspects Comput., 2023)

Detecting Speculative Execution Vulnerabilities on Weak Memory Models. - Nicholas Coughlin; Kait Lam; Graeme Smith 001; Kirsten Winter (FM (1), 2024)