Kirsten Winter
|
Research Fellow |
|
Publications
Book or Book Chapter
Carlo A. Furia, Kirsten Winter:
Integrated Formal Methods - 14th International Conference, IFM 2018,
Maynooth, Ireland, September 5-7, 2018, Proceedings.
Lecture Notes in Computer Science 11023, Springer 2018, ISBN 978-3-319-98937-2
Integrated Formal Methods - 14th International Conference, IFM 2018,
Maynooth, Ireland, September 5-7, 2018, Proceedings.
Lecture Notes in Computer Science 11023, Springer 2018, ISBN 978-3-319-98937-2
Kirsten Winter
Symbolic Model Checking for Interlocking Systems.
In F. Flammini Railway Safety, Reliability, and Security:
Technologies and Systems Engineering.
pages 298-315, (Chapter 13), IGI Global, 2012.
Symbolic Model Checking for Interlocking Systems.
In F. Flammini Railway Safety, Reliability, and Security:
Technologies and Systems Engineering.
pages 298-315, (Chapter 13), IGI Global, 2012.
Journal Publications
N. Coughlin and K. Winter and G. Smith:
Compositional reasoning for non-multicopy atomic architectures .
in Formal Aspects of Computing, Volume 35 Issue 2, Springer-Verlag, 2023.
Compositional reasoning for non-multicopy atomic architectures .
in Formal Aspects of Computing, Volume 35 Issue 2, Springer-Verlag, 2023.
G. Smith and K. Winter:
Linearizability on hardware weak memory models.
in Formal Aspects of Computing, Volume 32, pages 1-32, Springer-Verlag 2020.
Linearizability on hardware weak memory models.
in Formal Aspects of Computing, Volume 32, pages 1-32, Springer-Verlag 2020.
K. Winter, G. Smith and J. Derrick:
Modelling concurrent objects running on the TSO and ARMv8 memory models.
in Science of Computer Programming, Volume 184,
pages 1-20, Elsevier, October 2019.
Modelling concurrent objects running on the TSO and ARMv8 memory models.
in Science of Computer Programming, Volume 184,
pages 1-20, Elsevier, October 2019.
I. J. Hayes, L. Meinicke, K. Winter, R. J. Colvin:
A synchronous program algebra:
a basis for reasoning about shared-memory and event-based concurrency.
in Formal Aspects of Computing, Volume 31, Issue 2,
pages 133-163, Springer-Verlag, April, 2019.
Extended versions of papers presented at FM 2016.
https://doi.org/10.1007/s00165-018-0464-4
A synchronous program algebra:
a basis for reasoning about shared-memory and event-based concurrency.
in Formal Aspects of Computing, Volume 31, Issue 2,
pages 133-163, Springer-Verlag, April, 2019.
Extended versions of papers presented at FM 2016.
https://doi.org/10.1007/s00165-018-0464-4
G. Smith and K. Winter:
Relating trace refinement and linearizability.
in Formal Aspects of Computing, Volume 29, Issue 6 (2017),
pages 935-950, Springer-Verlag, November, 2017.
Relating trace refinement and linearizability.
in Formal Aspects of Computing, Volume 29, Issue 6 (2017),
pages 935-950, Springer-Verlag, November, 2017.
N. Yatapanage and K. Winter:
Next-preserving Branching Bisimulation.
in Theoretical Computer Science , Volume 594 (23 August 2015),
pages 120-142, Elsevier, August, 2015.
Next-preserving Branching Bisimulation.
in Theoretical Computer Science , Volume 594 (23 August 2015),
pages 120-142, Elsevier, August, 2015.
G. Smith, J.W. Sanders and K. Winter:
Designing adaptive systems using teleo-reactive agents.
in Transactions on Computational Collective Intelligence XVI,
Volume 8780 of Lecture Notes in Computer Science. Springer-Verlag, 2014.
Designing adaptive systems using teleo-reactive agents.
in Transactions on Computational Collective Intelligence XVI,
Volume 8780 of Lecture Notes in Computer Science. Springer-Verlag, 2014.
P. Lindsay and N. Yatapanage and K. Winter:
Cut Set Analysis using Behavior Trees and model checking.
in Formal Aspects of Computing, Volume 24, Issue 2 (2012),
pages 249-266, Springer-Verlag, February, 2012.
Cut Set Analysis using Behavior Trees and model checking.
in Formal Aspects of Computing, Volume 24, Issue 2 (2012),
pages 249-266, Springer-Verlag, February, 2012.
L. Grunske and K. Winter and N. Yatapanage and S. Zafar and
P. A. Lindsay:
Experience with Fault Injection Experiments for FMEA.
in Software: Practice and Experience,
Volume 41, Number 11, pages 1233-1258, Wiley Ltd., January, 2011.
Experience with Fault Injection Experiments for FMEA.
in Software: Practice and Experience,
Volume 41, Number 11, pages 1233-1258, Wiley Ltd., January, 2011.
G. Smith and K. Winter:
Model checking action system refinements.
in Formal Aspects of Computing, Volume 21, Issue 1 (2009),
pages 155-186, Springer-Verlag, February, 2009.
Model checking action system refinements.
in Formal Aspects of Computing, Volume 21, Issue 1 (2009),
pages 155-186, Springer-Verlag, February, 2009.
R. Colvin and L. Grunske and K. Winter:
Timed Behavior Trees for Failure Mode and Effects Analysis
of Time-Critical Systems.
in Journal of Systems and Software ,
Volume 81/12, pages 2163-2182, Elsevier, 2008.
Timed Behavior Trees for Failure Mode and Effects Analysis
of Time-Critical Systems.
in Journal of Systems and Software ,
Volume 81/12, pages 2163-2182, Elsevier, 2008.
L. Grunske and K. Winter and N. Yatapanage
Defining the Abstract Syntax of Visual Languages with Advanced Graph Grammars -
A Case Study Based on Behavior Trees.
in Journal of Visual Languages and Computing,
Volume 19/3, pages 343-379, Elsevier, 2008.
Defining the Abstract Syntax of Visual Languages with Advanced Graph Grammars -
A Case Study Based on Behavior Trees.
in Journal of Visual Languages and Computing,
Volume 19/3, pages 343-379, Elsevier, 2008.
A. Gawanmeha and S. Tahara and K. Winter
Formal verification of ASMs using MDGs.
in Journal of Systems Architecture,
Volume 54, Issues 1-2, pages 15-34, Elsevier, 2008.
Formal verification of ASMs using MDGs.
in Journal of Systems Architecture,
Volume 54, Issues 1-2, pages 15-34, Elsevier, 2008.
Kirsten Winter:
Modelchecking for Abstract State Machines.
in Journal of Universal Computer Science,
Volume 3, Number 5, pages 689-701, 1997.
Modelchecking for Abstract State Machines.
in Journal of Universal Computer Science,
Volume 3, Number 5, pages 689-701, 1997.
Refereed Conference Publications
N. Coughlin, K. Lam, G. Smith and K. Winter:
Detecting Speculative Execution Vulnerabilities on Weak Memory Models.
In A. Platzer, K.Y. Rozier, M. Pradella, M. Rossi (Eds.):
International Symposium on Formal Methods. FM 2024 .
volume 14933 of Lecture Notes in Computer Science, pages 482-500.
© Springer-Verlag Berlin Heidelberg 2024 (the final publication is available at www.springer.com)
Detecting Speculative Execution Vulnerabilities on Weak Memory Models.
In A. Platzer, K.Y. Rozier, M. Pradella, M. Rossi (Eds.):
International Symposium on Formal Methods. FM 2024 .
volume 14933 of Lecture Notes in Computer Science, pages 482-500.
© Springer-Verlag Berlin Heidelberg 2024 (the final publication is available at www.springer.com)
N. Coughlin, K. Winter and G. Smith:
Rely/guarantee reasoning for multicopy atomic weak memory models.
In M. Huismann and C. S. Pasareanu and N. Zhan (Eds.):
International Symposium on Formal Methods (FM 2021)
volume 13047 of Lecture Notes in Computer Science, pages 292-310
© Springer-Verlag Berlin Heidelberg 2021 (the final publication is available at www.springer.com)
Best Paper Award at FM 2021.
Rely/guarantee reasoning for multicopy atomic weak memory models.
In M. Huismann and C. S. Pasareanu and N. Zhan (Eds.):
International Symposium on Formal Methods (FM 2021)
volume 13047 of Lecture Notes in Computer Science, pages 292-310
© Springer-Verlag Berlin Heidelberg 2021 (the final publication is available at www.springer.com)
Best Paper Award at FM 2021.
K. Winter, N. Coughlin and G. Smith:
Backwards-directed information flow analysis for concurrent programs.
In IEEE Computer Security Foundations Symposium (CSF 2021) IEEE, 2021.
Backwards-directed information flow analysis for concurrent programs.
In IEEE Computer Security Foundations Symposium (CSF 2021) IEEE, 2021.
R. Colvin and K. Winter:
An abstract semantics of speculative execution for reasoning about security vulnerabilities.
in Formal Methods (FM) 2019 International Workshops
volume 12233 of Lecture Note in Computer Science,
pages 323-341, Springer-Verlag, 2019.
An abstract semantics of speculative execution for reasoning about security vulnerabilities.
in Formal Methods (FM) 2019 International Workshops
volume 12233 of Lecture Note in Computer Science,
pages 323-341, Springer-Verlag, 2019.
K. Winter, G. Smith, and J. Derrick:
Observational models for linearizability checking on weak memory models .
in 12th International Symposium on Theoretical Aspects of Software Engineering (TASE 2018)
© IEEE Computer Society Press, 2018.
Observational models for linearizability checking on weak memory models .
in 12th International Symposium on Theoretical Aspects of Software Engineering (TASE 2018)
© IEEE Computer Society Press, 2018.
I.J. Hayes, R.J. Colvin, L.A. Meinicke, K. Winter, A.
Velykis:
An algebra of synchronous atomic steps
In J. Fitzgerald and S. Gnesi and C. Heitmeyer (Eds.):
International Symposium on Formal Methods (FM 2016) .
Lecture Notes in Computer Science, Springer-Verlag, 2016.
Best Paper Award at FM 2016.
An algebra of synchronous atomic steps
In J. Fitzgerald and S. Gnesi and C. Heitmeyer (Eds.):
International Symposium on Formal Methods (FM 2016) .
Lecture Notes in Computer Science, Springer-Verlag, 2016.
Best Paper Award at FM 2016.
K. Winter, C. Zhang, I.J. Hayes, N. Keynes, C. Cifuentes,
L. Li:
Path-Sensitive Data Flow Analysis Simplified
In L. Groves, L. Jun (Eds.): Intenational Conference on Formal Engineering Methods (ICFEM 2013).
volume 8144 of Lecture Notes in Computer Science, pages 415 - 430
© Springer-Verlag Berlin Heidelberg 2013 (the final publication is available at www.springer.com)
Path-Sensitive Data Flow Analysis Simplified
In L. Groves, L. Jun (Eds.): Intenational Conference on Formal Engineering Methods (ICFEM 2013).
volume 8144 of Lecture Notes in Computer Science, pages 415 - 430
© Springer-Verlag Berlin Heidelberg 2013 (the final publication is available at www.springer.com)
K. Winter:
Optimising Ordering Strategies for Symbolic Model Checking of Railway Interlockings
In T. Margaria, B. Steffen, and M. Merten (Eds.):
Symposium On Leveraging Applications of Formal Methods, Verification and Validation
(ISoLA 2012), Part II , volume 7610 of Lecture Notes in Computer Science, pages 246 - 260
© Springer-Verlag Berlin Heidelberg 2012 (the final publication is available at www.springer.com)
Optimising Ordering Strategies for Symbolic Model Checking of Railway Interlockings
In T. Margaria, B. Steffen, and M. Merten (Eds.):
Symposium On Leveraging Applications of Formal Methods, Verification and Validation
(ISoLA 2012), Part II , volume 7610 of Lecture Notes in Computer Science, pages 246 - 260
© Springer-Verlag Berlin Heidelberg 2012 (the final publication is available at www.springer.com)
G. Smith and K. Winter:
Incremental development of multi-agent systems in Object-Z.
In Software Engineering Workshop (SEW-35).
© IEEE Computer Society Press, 2012.
Incremental development of multi-agent systems in Object-Z.
In Software Engineering Workshop (SEW-35).
© IEEE Computer Society Press, 2012.
G. Smith and J.W. Sanders and K. Winter:
Reasoning about adaptivity of agents and multi-agent systems.
In IEEE Intenational Conference on Engineering of Complex Computer Systems (ICECCS 2012).
pages 341 - 350, IEEE Computer Society Press, 2012.
Reasoning about adaptivity of agents and multi-agent systems.
In IEEE Intenational Conference on Engineering of Complex Computer Systems (ICECCS 2012).
pages 341 - 350, IEEE Computer Society Press, 2012.
K. Winter and I. J. Hayes and R. Colvin:
Integrating Requirements: The Behavior Tree Philosophy
In Proc. of Software Engineering and Formal Methods (SEFM 2010),
pages 41 - 50, IEEE Computer Society, 2010.
© IEEE Computer Society Press, 2010.
Integrating Requirements: The Behavior Tree Philosophy
In Proc. of Software Engineering and Formal Methods (SEFM 2010),
pages 41 - 50, IEEE Computer Society, 2010.
© IEEE Computer Society Press, 2010.
P. A. Lindsay and K. Winter and N. Yatapanage:
Safety Assessment using Behavior Trees and Model Checking
In Proc. of Software Engineering and Formal Methods (SEFM 2010),
pages 181 - 190, IEEE Computer Society, 2010.
© IEEE Computer Society Press, 2010.
Safety Assessment using Behavior Trees and Model Checking
In Proc. of Software Engineering and Formal Methods (SEFM 2010),
pages 181 - 190, IEEE Computer Society, 2010.
© IEEE Computer Society Press, 2010.
N. Yatapanage and K. Winter:
Slicing Behavior Tree Models for Verification
In C. S. Calude and V. Sassone (Eds.) Proc. of Theoretical Computer Science (TCS 2010) ,
pages 125 - 139, IFIP AICT 323, 2010.
© IFIP International Federation for Information Processing 2010.
Slicing Behavior Tree Models for Verification
In C. S. Calude and V. Sassone (Eds.) Proc. of Theoretical Computer Science (TCS 2010) ,
pages 125 - 139, IFIP AICT 323, 2010.
© IFIP International Federation for Information Processing 2010.
K. Winter and R. Colvin and R. G. Dromey:
Dynamic Relational Behaviour for Large-Scale Systems
In C. Fidge, Proc. of Australian Software Engineering Conference (ASWEC 2009),
pages 173-182, IEEE Computer Society, 2009.
Dynamic Relational Behaviour for Large-Scale Systems
In C. Fidge, Proc. of Australian Software Engineering Conference (ASWEC 2009),
pages 173-182, IEEE Computer Society, 2009.
L. van den Berg and P. Strooper and K. Winter:
Introducing Time in an Industrial Application of Model Checking.
In Proc. of 12th Int. ERCIM Workshop on Formal Methods for
Industrial Critical Systems (FMICS'07) ,
volume 4916 of Lecture Notes in Computer Science, pages 56-67.
Springer-Verlag, 2008.
Introducing Time in an Industrial Application of Model Checking.
In Proc. of 12th Int. ERCIM Workshop on Formal Methods for
Industrial Critical Systems (FMICS'07) ,
volume 4916 of Lecture Notes in Computer Science, pages 56-67.
Springer-Verlag, 2008.
L. Grunske and R. Colvin and K. Winter:
Probabilistic Model-Checking Support for FMEA.
In Proc. of 4th Int. Conf. on the Quantitative Evaluation of SysTems (QEST) 2007,
pages 119-128. IEEE Computer Society Press, 2007.
Probabilistic Model-Checking Support for FMEA.
In Proc. of 4th Int. Conf. on the Quantitative Evaluation of SysTems (QEST) 2007,
pages 119-128. IEEE Computer Society Press, 2007.
R. Colvin and L. Grunske and K. Winter:
Probabilistic Timed Behavior Trees.
In J. Davies and J. Gibbons, editors,
Proc. of 6th Int. Conf. on Integrated Formal Methods (IFM 2007),
volume 4591 of Lecture Notes in Computer Science, pages 156-175.
Springer-Verlag, 2007.
Probabilistic Timed Behavior Trees.
In J. Davies and J. Gibbons, editors,
Proc. of 6th Int. Conf. on Integrated Formal Methods (IFM 2007),
volume 4591 of Lecture Notes in Computer Science, pages 156-175.
Springer-Verlag, 2007.
L. Grunske and K. Winter and R. Colvin:
Timed Behavior Trees and their Application to Verifying Real-time Systems.
In J. Grundy and J. Han, editors,
Proc. of 18th Australian Conference on Software Engineering (ASWEC 2007),
pages 211-222, IEEE Computer Society, 2007.
Timed Behavior Trees and their Application to Verifying Real-time Systems.
In J. Grundy and J. Han, editors,
Proc. of 18th Australian Conference on Software Engineering (ASWEC 2007),
pages 211-222, IEEE Computer Society, 2007.
S. Zafar and R. Colvin and K. Winter and N. Yatapanage and
G. Dromey:
Early Validation and Verification of a Distributed Role-Based Access Control Model.
In Proc. of 14th Asia-Pacific Software Engineering Conference (APSEC 2007),
pages 430-437, IEEE Computer Society, 2007.
Early Validation and Verification of a Distributed Role-Based Access Control Model.
In Proc. of 14th Asia-Pacific Software Engineering Conference (APSEC 2007),
pages 430-437, IEEE Computer Society, 2007.
G. Smith and K. Winter:
Simulation machines for checking action system refinements.
In B. Aichernig, E. Boiten, J. Derrick and L. Groves, (eds.),
International Refinement Workshop (Refine 2006),
Electronic Notes in Theoretical Computer Science. Elsevier, 2006.
(available as Technical Report SSE-2006-03)
Simulation machines for checking action system refinements.
In B. Aichernig, E. Boiten, J. Derrick and L. Groves, (eds.),
International Refinement Workshop (Refine 2006),
Electronic Notes in Theoretical Computer Science. Elsevier, 2006.
(available as Technical Report SSE-2006-03)
W. Johnston, K. Winter, L. van den Berg, P. Strooper, P.
Robinson:
Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking.
In J. Misra, T. Nipkow, E. Sekerinski, editors,
14th International Symposium on Formal Methods (FM 2006)
volume 4085 of Lecture Notes in Computer Science, pages 524 - 540.
Springer-Verlag, 2006.
(electronically available at Springer)
Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking.
In J. Misra, T. Nipkow, E. Sekerinski, editors,
14th International Symposium on Formal Methods (FM 2006)
volume 4085 of Lecture Notes in Computer Science, pages 524 - 540.
Springer-Verlag, 2006.
(electronically available at Springer)
L. Grunske, P. Lindsay, N. Yatapanage, K. Winter:
An Automated Failure Mode and Effect Analysis based on
High-Level Design Specification with Behavior Trees
In J. Romijn, G. Smith and J. van de Pol, editors,
5th Int. Conf. on Integrated Formal Methods (IFM 2005),
volume 3771 of Lecture Notes in Computer Science, pages 129-149.
Springer-Verlag, 2005.
An Automated Failure Mode and Effect Analysis based on
High-Level Design Specification with Behavior Trees
In J. Romijn, G. Smith and J. van de Pol, editors,
5th Int. Conf. on Integrated Formal Methods (IFM 2005),
volume 3771 of Lecture Notes in Computer Science, pages 129-149.
Springer-Verlag, 2005.
K. Winter, W. Johnston, P. Robinson, P. Strooper, L. van
den Berg:
Tool Support for Checking Railway Interlocking Designs
In T. Cant, editor, 10th Australian Workshop on
Safety Related Programmable Systems (SCS'05)
Australian Computer Society, Inc., volume 55, 2005.
Tool Support for Checking Railway Interlocking Designs
In T. Cant, editor, 10th Australian Workshop on
Safety Related Programmable Systems (SCS'05)
Australian Computer Society, Inc., volume 55, 2005.
Kirsten Winter:
Formalising Behaviour Trees with CSP
In E. Boiten, J. Derrick, G. Smith, editors,
4th Int. Conf. on Integrated Formal Methods (IFM 2004),
volume 2999 of Lecture Notes in Computer Science, pages 148-167.
Springer-Verlag, 2004.
Formalising Behaviour Trees with CSP
In E. Boiten, J. Derrick, G. Smith, editors,
4th Int. Conf. on Integrated Formal Methods (IFM 2004),
volume 2999 of Lecture Notes in Computer Science, pages 148-167.
Springer-Verlag, 2004.
Amjad Gawanmeh, Sofiene Tahar, Kirsten Winter:
Formal Verification of ASM Designs using the MDG Tool
In A. Cerone, P. Lindsay, editors,
Int. Conf. on Software Engineering and Formal Methods (SEFM 2003),
pages 210-219, IEEE Computer Society, 2003.
Formal Verification of ASM Designs using the MDG Tool
In A. Cerone, P. Lindsay, editors,
Int. Conf. on Software Engineering and Formal Methods (SEFM 2003),
pages 210-219, IEEE Computer Society, 2003.
Kirsten Winter, Graeme Smith:
Compositional Verification for Object-Z
In D. Bert, J.P. Bowen, S. King and M. Walden, editors,
3rd Int. Conference of Z and B Users (ZB 2003), volume 2561
of Lecture Notes in Computer Science, pages 280-299. Springer-Verlag, 2003.
Compositional Verification for Object-Z
In D. Bert, J.P. Bowen, S. King and M. Walden, editors,
3rd Int. Conference of Z and B Users (ZB 2003), volume 2561
of Lecture Notes in Computer Science, pages 280-299. Springer-Verlag, 2003.
Graeme Smith, Kirsten Winter:
Proving temporal properties of Z specifications using abstraction
In D. Bert, J.P. Bowen, S. King and M. Walden, editors,
3rd Int. Conference of Z and B Users (ZB 2003), volume 2561
of Lecture Notes in Computer Science, pages 260-279. Springer-Verlag, 2003.
Proving temporal properties of Z specifications using abstraction
In D. Bert, J.P. Bowen, S. King and M. Walden, editors,
3rd Int. Conference of Z and B Users (ZB 2003), volume 2561
of Lecture Notes in Computer Science, pages 260-279. Springer-Verlag, 2003.
Kirsten Winter, Neil J. Robinson:
Modelling Large Interlocking Systems and Model Checking Small Ones
In M. Oudshoorn (ed.), 26th Australasian Computer Science Conference (ACSC 2003),
Australian Computer Science Communications, Vol. 16, 2003.
(also as Technical Report)
Modelling Large Interlocking Systems and Model Checking Small Ones
In M. Oudshoorn (ed.), 26th Australasian Computer Science Conference (ACSC 2003),
Australian Computer Science Communications, Vol. 16, 2003.
(also as Technical Report)
Amjad Gawanmeh, Sofiene Tahar, Kirsten Winter:
Interfacing ASMs with the MDG tool
In E. Börger, A. Gargantini, E. Riccobene (eds.),
9th International Workshop on Abstract State Machines (ASM 2003)
volume 2589 of Lecture Notes in Computer Science, pages 278-292. Springer-Verlag, 2003.
Interfacing ASMs with the MDG tool
In E. Börger, A. Gargantini, E. Riccobene (eds.),
9th International Workshop on Abstract State Machines (ASM 2003)
volume 2589 of Lecture Notes in Computer Science, pages 278-292. Springer-Verlag, 2003.
Kirsten Winter, Roger Duke:
Model Checking Object-Z using ASM
In K. Sere and M. Butler (eds.), 3rd Int. Conf. on Integrated Formal Methods (IFM 2002) ,
volume 2335 of Lecture Notes in Computer Science, pages 165-184. Springer-Verlag, 2002.
(also as Technical Report)
Model Checking Object-Z using ASM
In K. Sere and M. Butler (eds.), 3rd Int. Conf. on Integrated Formal Methods (IFM 2002) ,
volume 2335 of Lecture Notes in Computer Science, pages 165-184. Springer-Verlag, 2002.
(also as Technical Report)
Kirsten Winter:
Model Checking Railway Interlocking Systems
In M. Oudshoorn (ed.), Proc. of Australian Computer Science Conference (ACSC 2002) ,
Australian Computer Science Communications, vol. 24(1), 2002.
(also as Technical Report)
Model Checking Railway Interlocking Systems
In M. Oudshoorn (ed.), Proc. of Australian Computer Science Conference (ACSC 2002) ,
Australian Computer Science Communications, vol. 24(1), 2002.
(also as Technical Report)
Kirsten Winter:
Model Checking with Abstract Types
Electronic Notes in Theoretical Computer Science 55, No. 3, 2001.
(also as Technical Report)
Model Checking with Abstract Types
Electronic Notes in Theoretical Computer Science 55, No. 3, 2001.
(also as Technical Report)
Giuseppe Del Castillo, Kirsten Winter:
Model Checking Support for the ASM High-Level Language.
In S. Graf, M. Schwartzbach (eds.), Proceedings of 6th Int. Conference TACAS 2000,
LNCS 1785, pp. 331-346, Springer-Verlag, 2000.
Abstract.
Model Checking Support for the ASM High-Level Language.
In S. Graf, M. Schwartzbach (eds.), Proceedings of 6th Int. Conference TACAS 2000,
LNCS 1785, pp. 331-346, Springer-Verlag, 2000.
Abstract.
Kirsten Winter:
Towards a Methodology for Model Checking ASM: Lessons learned from the FLASH Case Study
In Y. Gurevich, P. Kutter, M. Odersky, L. Thiele (eds.),
Proceedings of International Workshop on Abstract State Machines (ASM 2000) ,
volume 1912 of Lecture Notes
on Computer Science, Springer-Verlag, pages 341-360, 2000.
Abstract.
Towards a Methodology for Model Checking ASM: Lessons learned from the FLASH Case Study
In Y. Gurevich, P. Kutter, M. Odersky, L. Thiele (eds.),
Proceedings of International Workshop on Abstract State Machines (ASM 2000) ,
volume 1912 of Lecture Notes
on Computer Science, Springer-Verlag, pages 341-360, 2000.
Abstract.
A.G. Bahmurov, V.I. Chervin, M.V.Chistolinov,
J.F.Groote,
V.A. Kostenko, R.L.Smeliansky, D.V.Tsarkov, Y.S.Usenko,
K.Winter, V.A.Zakharov.
Towards a Unified Toolset for Embedded Systems Development
Special Issue of the Scientific Journal "Problems of Programming"
No 1-2, pages 316-322, 2000.
V.A. Kostenko, R.L.Smeliansky, D.V.Tsarkov, Y.S.Usenko,
K.Winter, V.A.Zakharov.
Towards a Unified Toolset for Embedded Systems Development
Special Issue of the Scientific Journal "Problems of Programming"
No 1-2, pages 316-322, 2000.
Kirsten Winter, Thomas Santen, Maritta Heisel:
Specifying the Safety Controllers of Traffic Light Systems in Z and Statecharts.
In F. Saglietti, W. Goerigk (eds.), Proc. Sicherheit und Zuverlässigkeit software-basierter Systeme,
Technical Report ISTec-A-367,
pp. 126-137, ISTec GmbH, 1999.
Specifying the Safety Controllers of Traffic Light Systems in Z and Statecharts.
In F. Saglietti, W. Goerigk (eds.), Proc. Sicherheit und Zuverlässigkeit software-basierter Systeme,
Technical Report ISTec-A-367,
pp. 126-137, ISTec GmbH, 1999.
Kirsten Winter, Thomas Santen, Maritta Heisel:
An Agenda for Specifying Software Components with Complex Data Model
In W. Ehrenberger (ed.), Proceedings of the 17th Int. Conference on
Computer Safety, Reliability and Security (SAFECOMP '98),
LNCS 1516, pages. 16-32, Springer-Verlag, 1998.
Abstract.
An Agenda for Specifying Software Components with Complex Data Model
In W. Ehrenberger (ed.), Proceedings of the 17th Int. Conference on
Computer Safety, Reliability and Security (SAFECOMP '98),
LNCS 1516, pages. 16-32, Springer-Verlag, 1998.
Abstract.
Unpublished Workshop Contributions, Technical Reports
Nisansala Yatapanage, Kirsten Winter
Next-preserving Branching Bisimulation
ITEE Technical Report 2013-02, The University of Queensland,
October 2013.
Next-preserving Branching Bisimulation
ITEE Technical Report 2013-02, The University of Queensland,
October 2013.
Kirsten Winter
Supporting Abstraction when Model Checking ASM
In Proceedings of Int. Conference on Computer Aided System Theory (EUROCAST 2001),
Las Palmas de Gran Canaria, Canary Island, 2001.
(also available as Technical Report 01-20 , Software Verification Research Centre,
University of Queensland, June 2001)
Supporting Abstraction when Model Checking ASM
In Proceedings of Int. Conference on Computer Aided System Theory (EUROCAST 2001),
Las Palmas de Gran Canaria, Canary Island, 2001.
(also available as Technical Report 01-20 , Software Verification Research Centre,
University of Queensland, June 2001)
J. Burghardt, S. Jaehnichen, F. Kammueller, C. Suehl, K.
Winter
Techniques of Rigorous Analysis,
In M. Wirsing, M. Gogolla, H.-J. Kreowski, T. Nipkow. W. Reif (eds.)
Rigorose Entwicklung software-intensiver Systeme
Workshop im Rahmen der GI Jahrestagung,
Technical Report LMU Munich, No. 0005, September, 2000.
(in German)
Techniques of Rigorous Analysis,
In M. Wirsing, M. Gogolla, H.-J. Kreowski, T. Nipkow. W. Reif (eds.)
Rigorose Entwicklung software-intensiver Systeme
Workshop im Rahmen der GI Jahrestagung,
Technical Report LMU Munich, No. 0005, September, 2000.
(in German)
Dissertation
Kirsten Winter:
Model Checking Abstract State Machines
Doctoral Dissertation accepted by:
Technical University of Berlin
School of Electrical Engineering and Computer Sciences
2001-07-17.
(in English)
Model Checking Abstract State Machines
Doctoral Dissertation accepted by:
Technical University of Berlin
School of Electrical Engineering and Computer Sciences
2001-07-17.
(in English)
