Dr Kirsten Winter

Research Fellow

School of Information Technology and Electrical Engineering
Faculty of Engineering, Architecture and Information Technology
kirsten@itee.uq.edu.au
+61 7 336 51629

Overview

Dr Kirsten Winter's research interests are in Formal methods and Automated reasoning: High-level specification languages (Object-Z and Abstract State Machines (ASM), CSP, Behavior Trees), Verification, Tool-supported analysis for high-level specification languages, Model checking and Abstraction and decomposition techniques, Static analysis, Program verification.

She received her PhD from Technical University, Germany, in 2001 and is currently employed as a research fellow at ITEE. Dr Winter's current research projects are in the fields of:

  • Model Checking and Static Analysis
  • Abstraction and decomposition techniques
  • Program Analysis and Bug Checking for large Code Bases

Qualifications

  • Master of Science, Erlangan-Nurnberg
  • Doctor in Philosphy, Technische Universität, Berlin

Publications

  • Smith, Graeme and Winter, Kirsten (2017) Relating trace refinement and linearizability. Formal Aspects of Computing, 1-16. doi:10.1007/s00165-017-0418-2

  • Hayes, Ian J., Colvin, Robert J., Meinicke, Larissa A., Winter, Kirsten and Velykis, Andrius (2016). An algebra of synchronous atomic steps. In: John Fitzgerald, Constance Heitmeyer, Stefania Gnesi and Anna Philippou, FM 2016: Formal Methods - 21st International Symposium, Proceedings. 21st International Symposium on Formal Methods, FM 2016, Limassol, Cyprus, (352-369). 9-11 November 2016. doi:10.1007/978-3-319-48989-6_22

  • Yatapanage, Nisansala and Winter, Kirsten (2015) Next-preserving branching bisimulation. Theoretical Computer Science, 594 120-142. doi:10.1016/j.tcs.2015.05.013

View all Publications

Publications

Book Chapter

  • Smith, Graeme, Sanders, J. W. and Winter, Kirsten (2014). Designing adaptive systems using teleo-reactive agents. In Ryszard Kowalczyk and Ngoc Thanh Nguyen (Ed.), Transactions on Computational Collective Intelligence XVI (pp. 34-61) Heidelberg, Germany: Springer. doi:10.1007/978-3-662-44871-7_2

  • Winter, Kirsten (2012). Symbolic model checking for interlocking systems. In Francesco Flammini (Ed.), Railway safety, reliability, and security: technologies and systems engineering (pp. 298-315) Hersey, PA, U.S.A.: IGI Global. doi:10.4018/978-1-4666-1643-1.ch013

Journal Article

Conference Publication

  • Hayes, Ian J., Colvin, Robert J., Meinicke, Larissa A., Winter, Kirsten and Velykis, Andrius (2016). An algebra of synchronous atomic steps. In: John Fitzgerald, Constance Heitmeyer, Stefania Gnesi and Anna Philippou, FM 2016: Formal Methods - 21st International Symposium, Proceedings. 21st International Symposium on Formal Methods, FM 2016, Limassol, Cyprus, (352-369). 9-11 November 2016. 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. In: Lindsay Groves and Jing Sun, Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods, ICFEM 2013, Proceedings. 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, (415-430). 29 October - 1 November 2013. doi:10.1007/978-3-642-41202-8_27

  • Smith, Graeme and Winter, Kirsten (2012). Incremental development of multi-agent systems in Object-Z. In: 35th Annual IEEE Software Engineeering Workshop (SEW-35): Proceedings. Software Engineering Workshop (SEW-35), Heraklion, Crete, Greece, (120-129). 12-13 October 2012. doi:10.1109/SEW.2012.19

  • Lindsay, Peter A., Winter, Kirsten and Kromodimoeljo, Sentot (2012). Model-based Safety Risk Assessment using Behaviour Trees. In: Peter A. Lindsay, Engineering/Test and Evaluation Conference and 6th Asia Pacific Conference on Systems Engineering, proceedings. Engineering/Test and Evaluation Conference and 6th Asia Pacific Conference on Systems Engineering (SETE APCOSE 2012), Brisbane, Qld., Australia, (). 1 - 2 May 2012.

  • Winter, Kirsten (2012). Optimising ordering strategies for symbolic model checking of railway interlockings. In: Tiziana Margaria and Bernhard Steffen, Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies: 5th International Symposium, ISoLA 2012. International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Heraklion, Crete, Greece, (246-260). 15-18 October 2012. doi:10.1007/978-3-642-34032-1_24

  • Smith, Graeme, Sanders, J. W. and Winter, Kirsten (2012). Reasoning about adaptivity of agents and multi-agent systems. In: CESAMES, Seventeenth IEEE International Conference on Engineering of Complex Computer Systems. IEEE Intenational Conference on Engineering of Complex Computer Systems, Paris, France, (341-350). 18-20 July 2012. doi:10.1109/ICECCS.2012.32

  • Winter, Kirsten, Hayes, Ian J. and Colvin, Robert (2010). Integrating requirements: The behavior tree philosophy. In: Proceedings of International Conference on Software Engineering and Formal Methods (SEFM 2010). Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, (41-50). 13-18 September 2010. doi:10.1109/SEFM.2010.13

  • Lindsay, Peter A., Winter, Kirsten and Yatapanage, Nisansala (2010). Safety assessment using behavior trees and model checking. In: 2010 8th IEEE International Conference on Software Engineering and Formal Methods. Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, (181-190). 13-18 September 2010. doi:10.1109/SEFM.2010.23

  • Yatapanage, Nisansala, Winter, Kirsten and Zafar, Saad (2010). Slicing behavior tree models for verification. In: Cristian S. Calude and Vladimiro Sassone, Proceedings of the 6th IFIP TC 1/WG 2.2 International Conference TCS 2010. 6th IFIP International Conference on Theoretical Computer Science, Brisbane, QLD, Australia, (125-139). 20-23 September 2010. 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. In: Colin Fidge, Proceedings of the 20th Australian Software Engineering Conference ASWEC 2009. 20th Australian Software Engineering Conference, Gold Coast, Australia, (173-182). 14-17 April, 2009. 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. In: Leue, S. and Merino, P., Lecture Notes in Computer Science ; Formal Methods for Industrial Critical Systems. 12th International Workshop on Formal Methods for Industrial Critical Systems, Berlin, Germany, (56-67). 1-2 July, 2008. doi:10.1007/978-3-540-79707-4_6

  • 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. In: Proceedings of the Software Engineering Conference 2007 (APSEC 2007). APSEC 2007: 14th Asia-Pacific Software Engineering Conference 2007, Nagoya, Japan, (430-437). 5-7 December 2007. doi:10.1109/ASPEC.2007.20

  • Grunske, L., Colvin, R. and Winter, K. (2007). Probabilistic model-checking support for FMEA. In: M. Harchol-Balter, M. Kwiatkowska and M. Telek, Proceedings Fourth International Conference on the Quantitative Evaluation of Systems. Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), Edinburgh, Scotland, (119-128). 17-19 September, 2007. doi:10.1109/QEST.2007.18

  • Colvin, Robert, Grunske, Lars and Winter, Kirsten (2007). Probabilistic timed behavior trees. In: J. Davies and J. Gibbons, Proceedings of the 6th International Conference IFM 2007 Integrated Formal Methods. Integrated Formal Methods 2007, Oxford, UK, (156-175). 2-5 July, 2007. doi:10.1007/978-3-540-73210-5_9

  • Smith, G. and Winter, K. (2007). Simulation machines for checking action system refinements. In: Aichernig, B., Boiten, E., Derrick, J. and Groves, L., Proceedings of the 11th Refinement Workshop (REFINE 2006). 11th Refinement Workshop (REFINE 2006), Macao, China, (75-90). 31 October 2006. doi:10.1016/j.entcs.2006.08.045

  • Grunske, Lars, Winter, Kirsten and Colvin, Robert (2007). Timed behavior trees and their application to verifying real-time systems. In: J. Grundy and J. Han, Proceedings of the 2007 Australian Conference on Software Engineering. Australian Conference on Software Engineering (ASWEC 2007), Melbourne, Australia, (211-222). 10-13 April 2007. doi:10.1109/ASWEC.2007.49

  • 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. In: Jayadev Misra, Tobias Nipkow and Emil Sekerinski, FM 2006: Formal Methods. 14th International Symposium on Formal Methods: Proceedings. Formal Methods 2006: 14th International Symposium on Formal Methods (FM 2006). Formal Methods for Security and Trust in Industrial Applications, Hamilton, ON, Canada, (524-540). 21-27 August 2006. doi:10.1007/11813040_35

  • Winter, K., Johnston, W., Robinson, P., Strooper, P. and van den Berg, L. (2005). Tool support for checking railway interlocking designs. In: , , (101-107). .

  • 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. In: Integrated Formal Methods: 5th International Conference. Integrated Formal Methods 2005, Eindhoven, The Netherlands, (129-149). 29 November - 2 December 2005.

  • Winter, K., Johnston, W. R., Robinson, P. J., Strooper, P. A. and Van Den Berg, L. (2005). Tool support for checking railway interlocking designs. In: Tony Cant, Proceedings of the 10th Australian Workshop on Safety Related Programmable Systems. 10th australian Workshop on Safety Related Programmable Systems (SCS'05), Sydney, Australia, (1-7). 25 -26 August 2005.

  • Smith, C., Winter, K., Hayes, I., Dromey, G., Lindsay, P. and Carrington, D. (2004). An environment for building a system out of its requirements. In: , , (398-399). . doi:10.1109/ASE.2004.1342775

  • Winter, Kirsten (2004). Formalising behaviour trees with CSP. In: E. Boiten, J. Derrick and G. Smith, Lecture Notes in Computer Science: Proceedings of the 4th International Conference on Integrated Formal Methods. 4th International Conference on Integrated Formal Methods, Canterbury, UK, (148-167). 4-7 April, 2004. doi:10.1007/b96106

  • Winter, Kirsten and Smith, Graeme P. (2003). Compositional verification for object-Z. In: D. Bert, J. Bowen, S. King and M. Walden, Lecture Notes in Computer Science: Proceedings of the 3rd International Conference on B and Z Users. The 3rd International Conference on B and Z Users, Turku, Finland, (280-299). 4-6 June, 2003. 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. In: A. Cerone and P. Lindsay, Proceedings of the First International Conference on Software Engineering and Formal Methods 2003. The First International Conference on Software Engineering and Formal Methods 2003, Brisbane, Australia, (210-219). 22-27 September 2003. doi:10.1109/SEFM.2003.1236223

  • Gawanmeh, Amjad, Tahar, Sofiène and Winter, Kirsten (2003). Interfacing ASM with the MDG tool. In: E. Borger, A. Gargantini and E. Riccobene, Lecture Notes in Computer Science: Abstract State Machines 2003. Abstract State Machines 2003 Advances in Theory and Practice 10th International Workshop, ASM 2003, Taormina, Italy, (278-292). 3-7 March, 2003. doi:10.1007/3-540-36498-6

  • Winter, K. and Robinson, N. J. (2003). Modelling large railway interlockings and model checking small ones. In: M. Oudshoorn, Computer Science 2003: Proceddings of the Twenty-Sixth Australasian Computer Science Conference. The Twenty-Sixth Australasian Computer Science Conference, Adelaide, (309-316). 4-7 February, 2003.

  • Smith, Graeme and Winter, Kirsten (2003). Proving Temporal Properties of Z Specifications Using Abstraction. In: D. Bert, J. P. Bowen, S. King and M. Waldén, ZB 2003: Formal Specification and Development in Z and B: Third International Conference of B and Z Users Turku, Finland, June 4–6, 2003 Proceedings. ZB 2003: Formal Specification and Development in Z and B : Third International Conference of B and Z Users, Turku, Finland, (260-279). 4–6 June 2003. doi:10.1007/3-540-44880-2_17

  • Winter, Kirsten (2002). Model Checking Railway Interlocking Systems. In: Computer Science 2002, Twenty-Fifth Australasian Computer Science Conference (ACSC2002). Australian Computer Science Conference (ACSC 2002), Melbourne, Australia, (303-310). 30 January - 3 February 2002.

  • Winter, K. and Duke, R. W. (2002). Model checking object-Z using ASM. In: M. Butler, L. Petre and K. Sere, proceedings of the Integrated Formal Methods 3rd International Conference, IFM 2002. Integrated Formal Methods 3rd International Conference, IFM 2002, Turku, Finland, (165-184). 15-18 May, 2002.

  • Winter, Kirsten (2001). Model Checking with Abstract Types. In: M. W. Mislove, Scott D. Stoller and Willem Visser, Electronic Notes in Theoretical Computer Science: Workshop on Software Model Checking (in connection with CAV '01). 13th Conference on Computer Aided Verification, Paris, France, (382-393). July 18-23, 2001. doi:10.1016/S1571-0661(04)00264-6

Other Outputs