Research Interests

I am a postdoc researcher working at the University of Innsbruck, working mainly on automated reasoning and term rewriting.

• Currently, I am working on a FWF Hertha Firnberg fellowship. The project is about Instantiation- and Learning-Based Methods in Equational Reasoning.
• Beforehand, I spent one year as a research developer at Microsoft Research, working on SMT-based compiler validation. I also spent some months there as a contractor, developing a verifier for the programming language Dafny called Selfy, which infers invariants automatically.
• Earlier, I was employed on the project Constrained Rewriting and SMT, contributing forbidden patterns and unraveling results to CeTA/IsaFor.
• For my PhD, I investigated variants of Knuth-Bendix completion combining a multi-completion approach with the use of automatic termination tools (this poster provides an overview).

Some code like the sources of the completion tools maedmax and mkbtt can be found on github.

CV

My CV can be found here.

Publications

Journal Articles

1. A. Yamada, S. Winkler, N. Hirokawa, and A. Middeldorp
   AC-KBO Revisited (preprint)
   Theory and Practice of Logic Programming 16(2), 19:1-19:16, 2016. © Cambridge University Press
2. H. Zankl, S. Winkler, and A. Middeldorp
   Beyond Polynomials and Peano Arithmetic – Automation of Elementary and Ordinal Interpretations (preprint)
   Journal of Symbolic Computation, 69, 129-158, 2015. © Elsevier
3. S. Winkler, H. Sato, A. Middeldorp, and M. Kurihara
   Multi-Completion with Termination Tools (preprint)
   Journal of Automated Reasoning, 50(3), 317-354, 2013. © Springer

Papers in Proceedings

1. C. Sternagel and S. Winkler.
   Certified equational reasoning via ordered completion
   In 27th CADE, LNCS 11716, pp. 508-525, 2019. ©Springer
2. S. Winkler.
   Extending maximal completion
   In FSCD 2019, LIPIcs 131, pp. 3:1-3:15, 2019. ©Creative Commons
3. N. Nishida and S. Winkler
   Loop Detection by Logically Constrained Term Rewriting
   In VSTTE 2018, LNCS 11294, pp. 309-321, 2018. ©Springer
4. S. Winkler and A. Middeldorp
   Completion for Logically Constrained Rewriting
   In FSCD 2018, LIPIcs 109, pp. 30:1-30:18, 2018. ©Creative Commons
5. S. Winkler and G. Moser
   MaedMax: A Maximal Ordered Completion Tool
   In IJCAR 2018, LNCS 10900, pp. 472-480, 2018. ©Springer-Verlag
6. N. Hirokawa, A. Middeldorp, C. Sternagel, and S. Winkler
   Infinite Runs in Abstract Completion
   In FSCD 2017, LIPIcs 84, pp. 19:1--19:16, 2017. ©Creative Commons
7. S. Winkler and R. Thiemann
   Formalizing Soundness and Completeness of Unravelings
   In FroCoS 2015, LNCS 9322, pp. 239-255, 2018. ©Springer-Verlag
8. H. Sato and S. Winkler
   Encoding DP Techniques and Control Strategies for Maximal Completion
   In CADE 25, to appear. LNCS 9195, pp 152-162, 2015. ©Springer-Verlag
9. T. Sternagel, S. Winkler, and H. Zankl
   Recording Completion for Certificates in Equational Reasoning
   In CPP 2015, ACM, pp. 41-47, 2015
10. J. Nagele, R. Thiemann, and S. Winkler
    Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
    In 6th VSTTE, LNCS 8471, pp. 216-232, 2014.
11. A. Yamada, S. Winkler, N. Hirokawa, and A. Middeldorp
    AC-KBO Revisited (report version)
    In 12th FLOPS, LNCS 8475, pp. 319-335, 2014.
12. S. Winkler and A. Middeldorp
    Normalized Completion Revisited
    In 24th RTA, LIPIcs 21, pp 319-334, 2013.
13. S. Winkler, H. Zankl, and A. Middeldorp
    Beyond Peano Arithmetic - Automatically Proving Termination of the Goodstein Sequence
    In 24th RTA, LIPIcs 21, pp 335-351, 2013.
14. S. Winkler, H. Zankl, and A. Middeldorp
    Ordinals and Knuth-Bendix Orders
    In LPAR-18, LNCS 7180, pp 420-434, 2012. ©Springer-Verlag
15. S. Winkler and A. Middeldorp
    AC Completion with Termination Tools
    In CADE 23, LNCS (LNAI) 6803, pp 492-498, 2011. ©Springer-Verlag
16. S. Winkler and A. Middeldorp
    Termination Tools in Ordered Completion
    In IJCAR 2010, LNCS (LNAI) 6173, pp. 518-532, 2010. ©Springer-Verlag
17. S. Winkler, H. Sato, A. Middeldorp, and M. Kurihara
    Optimizing mkbTT (System Description)
    In 21st RTA, LIPIcs 13, pp 373-384, 2010. Creative-Commons
18. H. Sato, S. Winkler, M. Kurihara, and A. Middeldorp
    Multi-completion with Termination Tools (System Description)
    In IJCAR 2008, LNCS (LNAI) 5195, pp. 306-312, 2008. ©Springer-Verlag

Thesis

1. S. Winkler
   Termination Tools in Automated Reasoning
   PhD thesis, University of Innsbruck, 2013.

Workshops

1. C. Sternagel and S. Winkler
   Certified Ordered Completion
   In Proceedings of the 7th International Workshop on Confluence (IWC 2018), pp 41-45, 2018.
2. S. Winkler
   A Ground Joinability Criterion for Ordered Completion
   In Proceedings of the 6th International Workshop on Confluence (IWC 2017), pp 45-50, 2017.
3. H. Sato and S. Winkler
   A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion
   In Proceedings of the 14th International Workshop on Termination (WST 2014),
   pp 80-84, 2014.
4. H. Zankl, S. Winkler and A. Middeldorp
   Automating Elementary Interpretations
   In Proceedings of the 14th International Workshop on Termination (WST 2014),
   pp 90-94, 2014.
5. H. Zankl, S. Winkler and A. Middeldorp
   Automating Ordinal Interpretations
   In Proceedings of the 12th International Workshop on Termination (WST 2012),
   pp 94-98, 2012.
6. H. Sato, S. Winkler, M. Kurihara, and A. Middeldorp
   Constraint-Based Multi-Completion Procedures for Term Rewriting Systems
   In IEICE Transactions on Information and Systems E92-D (2), pp 220-234, 2009
7. C. Sternagel, R. Thiemann, S. Winkler, and H. Zankl
   CeTA – A Tool for Certified Termination Analysis
   In Proceedings of the 10th International Workshop on Termination (WST 2009),
   pp 84-87, 2009.