sarah winkler

Universitá degli Studi di Verona // Ca' Vignal 2 // Strada le Grazie 15 // Verona

sarahmaria.winkler_at_univr.it

research
teaching
software
publications
talks

Research Interests

I am a postdoctoral researcher at Universitá degli Studi di Verona, working on automated reasoning.

Previously, I was an FWF Hertha Firnberg fellow at the University of Innsbruck working on a 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, to infer invariants automatically.

Even 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.

CV

My CV can be found here.

Research Keywords

Some code like the sources of the completion tools maedmax and mkbtt can be found on github.
The slides of some of my recent talks can be found here:

Journal Articles

  1. N. Hirokawa, A. Middeldorp, C. Sternagel, and S. Winkler
    Abstract Completion, Formalized (preprint)
    Logical Methods in Computer Science 15(3), 1:1-1:19, 2019. © Creative Commons
  2. 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
  3. 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
  4. 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

Conference 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
  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
  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
  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
  15. S. Winkler and A. Middeldorp
    AC Completion with Termination Tools
    In CADE 23, LNCS (LNAI) 6803, pp 492-498, 2011. ©Springer
  16. S. Winkler and A. Middeldorp
    Termination Tools in Ordered Completion
    In IJCAR 2010, LNCS (LNAI) 6173, pp. 518-532, 2010. ©Springer
  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

Thesis

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

Workshop Proceedings and Others

  1. S. Winkler and Aart Middeldorp
    Tools in Term Rewriting for Education
    In Postproceedings of Theorem Proving Components for Educational Software (ThEdu 2019), 2019, to appear.
  2. S. Winkler and G. Moser
    Smarter Features, Simpler Learning?
    In Postproceedings of Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019), 25-32, 2019.
  3. S. Winkler
    Maedmax at School
    In Proceedings of the 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019), pp 38-40, 2019.
  4. C. Sternagel and S. Winkler
    Certified Ordered Completion
    In Proceedings of the 7th International Workshop on Confluence (IWC 2018), pp 41-45, 2018.
  5. S. Winkler
    A Ground Joinability Criterion for Ordered Completion
    In Proceedings of the 6th International Workshop on Confluence (IWC 2017), pp 45-50, 2017.
  6. 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.
  7. 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.
  8. 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.
  9. 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
  10. 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.

International Summer School on Rewriting

Together with Aart Middeldorp I taught at several editions of the International Summer School on Rewriting:

Courses taught at the University of Innsbruck

Summer 2019

SAT and SMT Solving

Friday 13:15 - 15:00 in HSB8

Summer 2018

SAT and SMT Solving

Thursday 11:15 - 13:00 in HS11

Winter 2014

Proseminar - Formal Language and Automata Theory

Monday 10:15 - 11:00 in SR 12

Winter 2013

Proseminar - Formal Language and Automata Theory

Monday 10:15 - 11:00 in SR Container 1

Winter 2012

Proseminar - Term Rewriting

Monday 14:15 - 15:00 in HS 11


Proseminar - Formal Language and Automata Theory

Friday 12:15 - 13:00 in HS 10

Winter 2011

Proseminar - Term Rewriting

Monday 14:15 - 15:00 in SR 12


Proseminar - Formal Language and Automata Theory

Monday 14:15 - 15:00 in SR 12

Winter 2010

Term Rewriting (exercise part)

Friday 12:15 - 13:00 in HS 10

Winter 2009/2010

Term Rewriting (exercise part)

Monday 9:15 to 10:00 in HS 10

Proseminar - Einführung in die Informatik

Group 10, Monday 16:15 to 17:45 in SR 13

Proseminar - Funktionale Programmierung

Group 3, Friday 9:15 to 10:00 in SR 13

Summer 2009

Proseminar - Formal Languages and Automata Theory

Group 1, Tuesday 10:15 - 11:45 in HS D

Summer 2008

Proseminar - Algorithms and Data Structures

Group 4, Wednesday 12:15 - 13:45 in RR 25

Winter 2007/2008

Proseminar - Logic
  • Group 1, Wednesday 12:15 to 13:45 in HS 10
  • Group 2, Wednesday 14:15 to 15:45 in HS 10

Summer 2007

Exercises - Formal Methods
  • Group 1, Monday 10:15 - 11:00 in SR 12
  • Group 2, Monday 11:15 - 12:00 in SR 12

Winter 2006/2007

Exercises - Logic

Group 1, Wednesday 11:15 - 12:00 in SR 12