Dr Kirsten Winter
Honorary Senior Fellow
School of Electrical Engineering and Computer Science
+61 7 336 51629
Featured projects | Duration |
---|---|
Program Analysis Cell | 2018 |
BASIL: Boogie Analysis for Secure Information-Flow Logics | 2022–2024 |
BAP ARMv8 Lifter Extension | 2022 |
Publications
Book Chapters
Coughlin, Nicholas, Lam, Kait, Smith, Graeme and Winter, Kirsten (2024). Detecting Speculative Execution Vulnerabilities on Weak Memory Models. Lecture Notes in Computer Science. (pp. 482-500) Cham: Springer Nature Switzerland. doi: 10.1007/978-3-031-71162-6_25
Smith, Graeme, Sanders, J. W. and Winter, Kirsten (2014). Designing adaptive systems using teleo-reactive agents. Transactions on Computational Collective Intelligence XVI. (pp. 34-61) edited by Ryszard Kowalczyk and Ngoc Thanh Nguyen. Heidelberg, Germany: Springer. doi: 10.1007/978-3-662-44871-7_2
Winter, Kirsten (2012). Symbolic model checking for interlocking systems. Railway safety, reliability, and security: technologies and systems engineering. (pp. 298-315) edited by Francesco Flammini. Hersey, PA, U.S.A.: IGI Global. doi: 10.4018/978-1-4666-1643-1.ch013
Journal Articles
Coughlin, Nicholas, Winter, Kirsten and Smith, Graeme (2023). Compositional reasoning for non-multicopy atomic architectures. Formal Aspects of Computing, 35 (2) 8, 1-30. doi: 10.1145/3574137
Smith, Graeme, Winter, Kirsten and Colvin, Robert J. (2019). Linearizability on hardware weak memory models. Formal Aspects of Computing, 32 (1), 1-32. doi: 10.1007/s00165-019-00499-8
Winter, Kirsten, Smith, Graeme and Derrick, John (2019). Modelling concurrent objects running on the TSO and ARMv8 memory models. Science of Computer Programming, 184 102308, 102308. doi: 10.1016/j.scico.2019.102308
Hayes, Ian J., Meinicke, Larissa A., Winter, Kirsten and Colvin, Robert J. (2018). A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Formal Aspects of Computing, 31 (2), 133-163. doi: 10.1007/s00165-018-0464-4
Smith, Graeme and Winter, Kirsten (2017). Relating trace refinement and linearizability. Formal Aspects of Computing, 29 (6), 1-16. doi: 10.1007/s00165-017-0418-2
Yatapanage, Nisansala and Winter, Kirsten (2015). Next-preserving branching bisimulation. Theoretical Computer Science, 594, 120-142. doi: 10.1016/j.tcs.2015.05.013
Lindsay, Peter A., Yatapanage, Nisansala and Winter, Kirsten (2012). Cut set analysis using behavior trees and model checking. Formal Aspects of Computing, 24 (2), 249-266. doi: 10.1007/s00165-011-0181-8
Grunske, Lars, Winter, Kirsten, Yatapanage, Nisansala, Zafar, Saad and Lindsay, Peter A. (2011). Experience with fault injection experiments for FMEA. Software: Practice and Experience, 41 (11), 1233-1258. doi: 10.1002/spe.1039
Smith, Graeme and Winter, Kirsten (2009). Model checking action system refinements. Formal Aspects of Computing, 21 (1-2), 155-186. doi: 10.1007/s00165-007-0053-4
Colvin, Robert, Grunske, Lars and Winter, Kirsten (2008). Timed behavior trees for failure mode and effects analysis of time-critical systems. Journal of Systems and Software, 81 (12), 2163-2182. doi: 10.1016/j.jss.2008.04.035
Grunske, Lars, Winter, Kirsten and Yatapanage, Nisansala (2008). Defining the abstract syntax of visual languages with advanced graph grammars: A case study based on behavior trees. Journal of Visual Languages and Computing, 19 (3), 343-379. doi: 10.1016/j.jvlc.2007.11.003
Gawanmeh, A, Tahar, S and Winter, K (2008). Formal verification of ASMs using MDGs. Journal of Systems Architecture, 54 (1-2), 15-34. doi: 10.1016/j.sysarc.2007.03.007
Smith, Graeme and Winter, Kirsten (2007). Simulation Machines for Checking Action System Refinements. Electronic Notes in Theoretical Computer Science, 187, 75-90. doi: 10.1016/j.entcs.2006.08.045
Conference Papers
Winter, Kirsten, Coughlin, Nicholas and Smith, Graeme (2021). Backwards-directed information flow analysis for concurrent programs. Computer Security Foundations Symposium, Dubrovnik, Croatia, 21-25 June 2021. Piscataway, NJ, United States: IEEE. doi: 10.1109/csf51468.2021.00017
Coughlin, Nicholas, Winter, Kirsten and Smith, Graeme (2021). Rely/guarantee reasoning for multicopy atomic weak memory models. 24th International Symposium on Formal Methods (FM), Virtual, 20-26 November 2021. Cham, Switzerland: Springer Science and Business Media Deutschland. doi: 10.1007/978-3-030-90870-6_16
Colvin, Robert J. and Winter, Kirsten (2020). An abstract semantics of speculative execution for reasoning about security vulnerabilities. Formal Methods. FM 2019 International Workshops, Porto, Portugal, 7–11 October 2019. Heidelberg, Germany: Springer. doi: 10.1007/978-3-030-54997-8_21
Furia, Carlo A. and Winter, Kirsten (2018). Preface. International Conference, IFM, Maynooth, Ireland, 5-7 September 2018. Heidelberg, Germany: Springer Verlag.
Smith, Graeme, Winter, Kirsten and Colvin, Robert J. (2018). Correctness of concurrent objects under weak memory models. 18th Refinement Workshop, Refine 2018, Oxford, United Kingdom, 18 July 2018. SYDNEY: Open Publishing Association. doi: 10.4204/EPTCS.282.5
Winter, Kirsten, Smith, Graeme and Derrick, John (2018). Observational models for linearizability checking on weak memory models. International Symposium on Theoretical Aspects of Software Engineering (TASE), Guangzhou, China, 29-31 August 2018. Piscataway, NJ United States: IEEE. doi: 10.1109/TASE.2018.00021
Hayes, Ian J., Colvin, Robert J., Meinicke, Larissa A., Winter, Kirsten and Velykis, Andrius (2016). An algebra of synchronous atomic steps. 21st International Symposium on Formal Methods, FM 2016, Limassol, Cyprus, 9-11 November 2016. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-48989-6_22
Winter, Kirsten, Zhang, Chenyi, Hayes, Ian J., Keynes, Nathan, Cifuentes, Cristina and Li, Lisa (2013). Path-sensitive data flow analysis simplified. 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, 29 October - 1 November 2013. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-41202-8_27
Smith, Graeme, Sanders, J. W. and Winter, Kirsten (2012). Reasoning about adaptivity of agents and multi-agent systems. IEEE Intenational Conference on Engineering of Complex Computer Systems, Paris, France, 18-20 July 2012. Piscataway, NJ, United States: IEEE Computer Society. doi: 10.1109/ICECCS.2012.32
Lindsay, Peter A., Winter, Kirsten and Kromodimoeljo, Sentot (2012). Model-based Safety Risk Assessment using Behaviour Trees. Engineering/Test and Evaluation Conference and 6th Asia Pacific Conference on Systems Engineering (SETE APCOSE 2012), Brisbane, Qld., Australia, 1 - 2 May 2012. Manuka, ACT, Australia: Systems Engineering Society of Australia.
Winter, Kirsten (2012). Optimising ordering strategies for symbolic model checking of railway interlockings. International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Heraklion, Crete, Greece, 15-18 October 2012. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-34032-1_24
Smith, Graeme and Winter, Kirsten (2012). Incremental development of multi-agent systems in Object-Z. Software Engineering Workshop (SEW-35), Heraklion, Crete, Greece, 12-13 October 2012. Piscataway, NJ, United States: IEEE Computer Society Press. doi: 10.1109/SEW.2012.19
Winter, Kirsten, Hayes, Ian J. and Colvin, Robert (2010). Integrating requirements: The behavior tree philosophy. Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, 13-18 September 2010. United States: IEEE Computer Society. doi: 10.1109/SEFM.2010.13
Lindsay, Peter A., Winter, Kirsten and Yatapanage, Nisansala (2010). Safety assessment using behavior trees and model checking. Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, 13-18 September 2010. Piscataway, NJ, United States: IEEE Computer Society Press. doi: 10.1109/SEFM.2010.23
Yatapanage, Nisansala, Winter, Kirsten and Zafar, Saad (2010). Slicing behavior tree models for verification. 6th IFIP International Conference on Theoretical Computer Science, Brisbane, QLD, Australia, 20-23 September 2010. Amsterdam, Netherlands: Elsevier. doi: 10.1007/978-3-642-15240-5_10
Winter, Kirsten, Colvin, Robert and Dromey, R, Geoff (2009). Dynamic relational behaviour for large-scale systems. 20th Australian Software Engineering Conference, Gold Coast, Australia, 14-17 April, 2009. U.S.A.: IEEE Computer Society Press. doi: 10.1109/ASWEC.2009.41
van den Berg, L., Strooper, P. and Winter, K. (2008). Introducing time in an industrial application of model-checking. 12th International Workshop on Formal Methods for Industrial Critical Systems, Berlin, Germany, 1-2 July, 2008. Berlin, Germany: Springer Verlag. doi: 10.1007/978-3-540-79707-4_6
Smith, G. and Winter, K. (2007). Simulation machines for checking action system refinements. 11th Refinement Workshop (REFINE 2006), Macao, China, 31 October 2006. USA: Elseiver BV. doi: 10.1016/j.entcs.2006.08.045
Zafar, Saad, Colvin, Robert, Winter, Kirsten, Yatapanage, Nisansala and Dromey, R.G. (2007). Early validation and verification of a distributed role-based access control model. APSEC 2007: 14th Asia-Pacific Software Engineering Conference 2007, Nagoya, Japan, 5-7 December 2007. Piscataway, NJ, United States: IEEE Computer Society. doi: 10.1109/ASPEC.2007.20
Grunske, L., Colvin, R. and Winter, K. (2007). Probabilistic model-checking support for FMEA. Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), Edinburgh, Scotland, 17-19 September, 2007. Los Alamitos, CA, USA: IEEE Computer Society. doi: 10.1109/QEST.2007.18
Grunske, Lars, Winter, Kirsten and Colvin, Robert (2007). Timed behavior trees and their application to verifying real-time systems. Australian Conference on Software Engineering (ASWEC 2007), Melbourne, Australia, 10-13 April 2007. Washington, DC, USA: IEEE Computer Society. doi: 10.1109/ASWEC.2007.49
Colvin, Robert, Grunske, Lars and Winter, Kirsten (2007). Probabilistic timed behavior trees. Integrated Formal Methods 2007, Oxford, UK, 2-5 July, 2007. New York, U.S.: Elsevier North-Holland. doi: 10.1007/978-3-540-73210-5_9
Johnston, Wendy, Winter, Kirsten, van den Berg, Lionel, Strooper, Paul and Robinson, Peter (2006). Model-based variable and transition orderings for efficient symbolic model checking. Formal Methods 2006: 14th International Symposium on Formal Methods (FM 2006). Formal Methods for Security and Trust in Industrial Applications, Hamilton, ON, Canada, 21-27 August 2006. Heidelberg, Germany: Springer Verlag. doi: 10.1007/11813040_35
Winter, K., Johnston, W. R., Robinson, P. J., Strooper, P. A. and Van Den Berg, L. (2005). Tool support for checking railway interlocking designs. 10th australian Workshop on Safety Related Programmable Systems (SCS'05), Sydney, Australia, 25 -26 August 2005. Sydney, Australia: Australian Computer Society Inc.
Grunske, Lars, Lindsay, Peter, Yatapanage, Nisansala and Winter, Kirsten (2005). An automated failure mode and effect analysis based on high-level design specificication with behavior trees. Integrated Formal Methods 2005, Eindhoven, The Netherlands, 29 November - 2 December 2005. Heidelberg, Germany: Springer. doi: 10.1007/11589976_9
Smith, C., Winter, K., Hayes, I., Dromey, G., Lindsay, P. and Carrington, D. (2004). An environment for building a system out of its requirements. Proceedings - 19th International Conference on Automated Software Engineering, ASE 2004, , , September 20, 2004-September 24, 2004. doi: 10.1109/ASE.2004.1342775
Winter, Kirsten (2004). Formalising behaviour trees with CSP. 4th International Conference on Integrated Formal Methods, Canterbury, UK, 4-7 April, 2004. Berlin: Springer-Verlag. doi: 10.1007/978-3-540-24756-2_9
Winter, K. and Robinson, N. J. (2003). Modelling large railway interlockings and model checking small ones. The Twenty-Sixth Australasian Computer Science Conference, Adelaide, 4-7 February, 2003. Sydney: Australian Computer Society.
Gawanmeh, Amjad, Tahar, Sofiène and Winter, Kirsten (2003). Interfacing ASM with the MDG tool. Abstract State Machines 2003 Advances in Theory and Practice 10th International Workshop, ASM 2003, Taormina, Italy, 3-7 March, 2003. Berlin: Springer-Verlag. doi: 10.1007/3-540-36498-6
Smith, Graeme and Winter, Kirsten (2003). Proving Temporal Properties of Z Specifications Using Abstraction. ZB 2003: Formal Specification and Development in Z and B : Third International Conference of B and Z Users, Turku, Finland, 4–6 June 2003. Heidelberg Germany: Springer - Verlag. doi: 10.1007/3-540-44880-2_17
Winter, Kirsten and Smith, Graeme P. (2003). Compositional verification for object-Z. The 3rd International Conference on B and Z Users, Turku, Finland, 4-6 June, 2003. Berlin: Springer-Verlag. doi: 10.1007/3-540-44880-2_18
Gawanmeh, A., Tahar, S. and Winter, K. (2003). Formal verification of ASM designs using the MDG tool. The First International Conference on Software Engineering and Formal Methods 2003, Brisbane, Australia, 22-27 September 2003. Los Alamitos, CA, U.S.A.: IEEE Computer Society. doi: 10.1109/SEFM.2003.1236223
Winter, Kirsten (2002). Model Checking Railway Interlocking Systems. Australian Computer Science Conference (ACSC 2002), Melbourne, Australia, 30 January - 3 February 2002. Australian Computer Science Communications.
Winter, K. and Duke, R. W. (2002). Model checking object-Z using ASM. Integrated Formal Methods 3rd International Conference, IFM 2002, Turku, Finland, 15-18 May, 2002. Berlin: Springer-Verlag. doi: 10.1007/3-540-47884-1_10
Winter, Kirsten (2001). Model Checking with Abstract Types. 13th Conference on Computer Aided Verification, Paris, France, July 18-23, 2001. Amsterdam ; New York: Elsevier Science. doi: 10.1016/S1571-0661(04)00264-6
Research Report
Winter, Kirsten (2001). Model checking with abstract types. SVRC Technical Report ; 01-16 University of Queensland, Brisbane: Software Verification Research Centre.
Department Technical Reports
Yatapanage, Nisansala and Winter, Kirsten (2013). Next-preserving branching bisimulation. ITEE Technical Report, 2013-02. School of Information Technology and Electrical Engineering, The University of Queensland.
Lindsay, Peter A., Winter, Kirsten and Colvin, Robert (2010). Model-checking tool support for quantitative risk analysis and design for safety. Division of Systems and Software Engineering Research, Technical Report SSE-2010-04. School of Information Technolology and Electrical Engineering, The University of Queensland.
Smith, Graeme and Winter, Kirsten (2006). Simulation Machines or Checking Action System Refinements. Technical Report No. SSE-2006-03. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.
Winter, Kirsten and Smith, Graeme (2002). Compositional Verification for Object-Z. Technical Report 02-42. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Winter, Kirsten (2001). Model Checking Railway Interlocking Systems. Technical Report 01-42. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Winter, Kirsten (2001). Supporting Abstraction when Model Checking ASM. Technical Report 01-20. Software Verification Research Centre, School of Information Technology, The University of Queensland.