Sarah Winkler  

Research Interests

My research interests focus on logic, automated reasoning and term rewriting. 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). For standard, ordered, and normalized completion I implemented this method in the tool mkbtt. I also worked on SMT encodings for the simple and elegant completion tool maxcomp, see here.
Recently, I was employed on the project Constrained Rewriting and SMT, contributing forbidden patterns and unraveling results to CeTA/IsaFor.
More recently, I did an internship at Microsoft Research Cambridge, developing a verifier for the programming language Dafny called Selfy, which can help you to find (loop) invariants.
Some code can also be found on github.

Publications

Journal Articles
  1. A. Yamada, S. Winkler, N. Hirokawa, and A. Middeldorp
    AC-KBO Revisited (preprint)
    Theory and Practice of Logic Programming, 2015. © 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. S. Winkler and R. Thiemann
    Formalizing Soundness and Completeness of Unravelings
    In FroCoS 2015, to appear.
  2. H. Sato and S. Winkler
    Encoding DP Techniques and Control Strategies for Maximal Completion
    In CADE 25, to appear.
  3. T. Sternagel, S. Winkler, and H. Zankl
    Recording Completion for Certificates in Equational Reasoning
    In CPP 2015, ACM, pp. 41-47, 2015
  4. 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.
  5. A. Yamada, S. Winkler, N. Hirokawa, and A. Middeldorp
    AC-KBO Revisited (report version)
    In 12th FLOPS, LNCS 8475, pp. 319-335, 2014.
  6. S. Winkler and A. Middeldorp
    Normalized Completion Revisited
    In 24th RTA, LIPIcs 21, pp 319-334, 2013.
  7. 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.
  8. S. Winkler, H. Zankl, and A. Middeldorp
    Ordinals and Knuth-Bendix Orders
    In LPAR-18, LNCS 7180, pp 420-434, 2012. ©Springer-Verlag
  9. S. Winkler and A. Middeldorp
    AC Completion with Termination Tools
    In CADE 23, LNCS (LNAI) 6803, pp 492-498, 2011. ©Springer-Verlag
  10. S. Winkler and A. Middeldorp
    Termination Tools in Ordered Completion
    In IJCAR 2010, LNCS (LNAI) 6173, pp. 518-532, 2010. ©Springer-Verlag
  11. S. Winkler, H. Sato, A. Middeldorp, and M. Kurihara
    Optimizing mkbTT (System Description)
    In 21st RTA, LIPIcs 13, pp 373-384, 2010. Creative-Commons
  12. 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. 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.
  2. 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.
  3. 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.
  4. 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
  5. 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.