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 LearningBased Methods in Equational Reasoning.

Beforehand, I spent one year as a research developer at Microsoft Research,
working on SMTbased 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 KnuthBendix completion
combining a multicompletion 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

A. Yamada, S. Winkler, N. Hirokawa, and A. Middeldorp
ACKBO Revisited
(preprint)
Theory and Practice of Logic Programming 16(2), 19:119:16, 2016.
© Cambridge University Press

H. Zankl, S. Winkler, and A. Middeldorp
Beyond Polynomials and Peano Arithmetic – Automation of Elementary and Ordinal Interpretations
(preprint)
Journal of Symbolic Computation, 69, 129158, 2015.
© Elsevier

S. Winkler, H. Sato, A. Middeldorp, and M. Kurihara
MultiCompletion with Termination Tools (preprint)
Journal of Automated Reasoning, 50(3), 317354, 2013.
© Springer
Papers in Proceedings

C. Sternagel and S. Winkler.
Certified equational reasoning via ordered completion
In 27th CADE,
LNCS 11716, pp. 508525, 2019.
©Springer

S. Winkler.
Extending maximal completion
In FSCD 2019,
LIPIcs 131, pp. 3:13:15, 2019.
©Creative Commons

N. Nishida and S. Winkler
Loop Detection by Logically Constrained Term Rewriting
In VSTTE 2018,
LNCS 11294, pp. 309321, 2018.
©Springer

S. Winkler and A. Middeldorp
Completion for Logically Constrained Rewriting
In FSCD 2018,
LIPIcs 109, pp. 30:130:18, 2018.
©Creative Commons

S. Winkler and G. Moser
MaedMax: A Maximal Ordered Completion Tool
In IJCAR 2018,
LNCS 10900, pp. 472480, 2018.
©SpringerVerlag

N. Hirokawa, A. Middeldorp, C. Sternagel, and S. Winkler
Infinite Runs in Abstract Completion
In FSCD 2017,
LIPIcs 84, pp. 19:119:16, 2017.
©Creative Commons

S. Winkler and R. Thiemann
Formalizing Soundness and Completeness of Unravelings
In FroCoS 2015,
LNCS 9322, pp. 239255, 2018.
©SpringerVerlag

H. Sato and S. Winkler
Encoding DP Techniques and Control Strategies for Maximal Completion
In CADE 25, to appear.
LNCS 9195, pp 152162, 2015.
©SpringerVerlag

T. Sternagel, S. Winkler, and H. Zankl
Recording Completion for Certificates in Equational Reasoning
In CPP 2015, ACM, pp. 4147, 2015

J. Nagele, R. Thiemann, and S. Winkler
Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
In 6th VSTTE, LNCS 8471, pp. 216232, 2014.

A. Yamada, S. Winkler, N. Hirokawa, and A. Middeldorp
ACKBO Revisited
(report version)
In 12th FLOPS,
LNCS 8475, pp. 319335, 2014.

S. Winkler and A. Middeldorp
Normalized Completion Revisited
In 24th RTA, LIPIcs 21, pp 319334, 2013.

S. Winkler, H. Zankl, and A. Middeldorp
Beyond Peano Arithmetic  Automatically Proving Termination of the Goodstein Sequence
In 24th RTA, LIPIcs 21, pp 335351, 2013.

S. Winkler, H. Zankl, and A. Middeldorp
Ordinals and KnuthBendix Orders
In LPAR18,
LNCS 7180, pp 420434, 2012.
©SpringerVerlag

S. Winkler and A. Middeldorp
AC Completion with Termination Tools
In CADE 23,
LNCS (LNAI) 6803, pp 492498, 2011.
©SpringerVerlag

S. Winkler and A. Middeldorp
Termination Tools in Ordered Completion
In IJCAR 2010,
LNCS (LNAI) 6173, pp. 518532, 2010.
©SpringerVerlag

S. Winkler, H. Sato, A. Middeldorp, and M. Kurihara
Optimizing mkbTT (System Description)
In 21st RTA,
LIPIcs 13, pp 373384, 2010.
CreativeCommons

H. Sato, S. Winkler, M. Kurihara, and A. Middeldorp
Multicompletion with Termination Tools (System Description)
In IJCAR 2008,
LNCS (LNAI) 5195, pp. 306312, 2008.
©SpringerVerlag
Thesis

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

C. Sternagel and S. Winkler
Certified Ordered Completion
In Proceedings of the 7th International Workshop on Confluence
(IWC 2018), pp 4145, 2018.

S. Winkler
A Ground Joinability Criterion for Ordered Completion
In Proceedings of the 6th International Workshop on Confluence
(IWC 2017), pp 4550, 2017.

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 8084, 2014.

H. Zankl, S. Winkler and A. Middeldorp
Automating Elementary Interpretations
In Proceedings of the 14th International Workshop on Termination
(WST 2014),
pp 9094, 2014.

H. Zankl, S. Winkler and A. Middeldorp
Automating Ordinal Interpretations
In Proceedings of the 12th International Workshop on Termination
(WST 2012),
pp 9498, 2012.

H. Sato, S. Winkler, M. Kurihara, and A. Middeldorp
ConstraintBased MultiCompletion Procedures for Term
Rewriting Systems
In IEICE Transactions on Information and Systems E92D (2), pp 220234, 2009

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 8487, 2009.