sarah winkler

Research Interests

• I am a postdoctoral researcher at the Free University of Bozen-Bolzano, working on verification of processes with data.
• Until August 2020, I was 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 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. For some months I also worked there as a contractor, developing the verifier Selfy for the programming language Dafny, to infer program 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.

Upcoming and Recent Events

• ISR 2024: 14th International School on Rewriting, 25.8.-1.9.2024, Obergurgl, Austria
• IJCAR 2024: 12th International Joint Conference on Automated Reasoning, 1.-6.7.2024, Nancy, France (PC)
• TACAS 2024: 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 6.-11.4.2024, Luxembourg (PC)
• BPM 2024: 22nd Business Process Management Conference, 1.-6.9.2024, Krakow (PC, publicity chair)
• CADE-29: 29th international Conference on Automated Deduction, 1.-4.7.2023, Rome, Italy (PC)
• FSCD 2023: 8th International Conference on Formal Structures for Computation and Deduction, 3.-6.7.2023, Rome, Italy (PC)
• IWC 2023: 12th International Workshop on Confluence (co-organizer), 23.8.2023, Obergurgl, Austria

CV

My CV can be found here.

Several software projects of which I am the main developer are described below. All are open source.

• Ada is a tool for LTL, CTL*, and soundness checking of Data Petri Nets and data-aware dynamic systems. Source code and a web interface are available.
• CoCoMoT is a conformance checker for Data Petri Nets. The source code is available on github.
• Koala is a first-order theorem prover based on semantically guided goal-sensitive reasoning. The source code is available on github.
• The completion tools maedmax and mkbtt can also be found on github.

• 10/2023 Decidable Fragments of LTLf Modulo Theories
  26th European Conference on Artificial Intelligence (ECAI 2023), Krakow, Poland
• 09/2023 Using Logic to Escape the Jungle of Data-aware Process Verification
  talk at the Technical University of Denmark, Copenhagen
• 07/2023 Approximating Multi-Perspective Trace Alignment Using Trace Encodings
  21st International Conference on Business Process Management (BPM 2023), Utrecht, Netherlands
• 02/2023 Monitoring Arithmetic Temporal Properties on Finite Traces
  37th AAAI Conference on Artificial Intelligence, Washington, USA
• 09/2020 Learning Strategy Design: First Lessons
  AITP 2020, Aussois, France
• 09/2020 Runtime Complexity Analysis of Logically Constrained Rewriting
  LOPSTR 2020, AoE
• 07/2020 SGGS Decision Procedures
  IJCAR-10, AoE
• 09/2019 Loop Detection by Logically Constrained Rewriting
  Dagstuhl Seminar 19371: Deduction Beyond Satisfiability, Wadern, Germany
• 08/2019 Certified Equational Reasoning via Ordered Completion
  CADE-27, Natal, Brazil
• 08/2019 Smarter Features, Simpler Learning?
  ARCADE 2019, Natal, Brazil
• 08/2019 Automation of Rewriting: for Fun in Research and Profit in Teaching
  ThEdu 2019, Natal, Brazil

Journal Articles

1. P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler
   Data-aware conformance checking with SMT
   Information Systems 117, 102230, 2023. doi: 10.1016/j.is.2023.102230
2. P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler
   Multi-perspective conformance checking of uncertain process traces: An SMT-based approach
   Engineering Applications of Artificial Intelligence 126(B):106895, 2023. doi: 10.1016/j.engappai.2023.106895
3. M.P. Bonacina and S. Winkler
   Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover
   Journal of Automated Reasoning, 2023. doi: 10.1007/s10817-022-09656-w
4. N. Hirokawa, A. Middeldorp, C. Sternagel, and S. Winkler
   Abstract Completion, Formalized
   Logical Methods in Computer Science 15(3), 2019. © Creative Commons
5. 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
6. 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
7. 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. P. Felli, M. Montali, and S. Winkler.
   Repairing Soundness Properties in Data-Aware Processes
   In ICPM 2023, IEEE 2023, pp. 41-48. doi: 10.1109/ICPM60904.2023.10271969
2. L. Geatti, A. Gianola, N. Gigante, S. Winkler.
   Decidable Fragments of LTLf Modulo Theories
   In ECAI 2023, 2023, IOS Press, FAIA 372, pp. 811-818. doi: 10.3233/FAIA230348
3. A. Gianola, J. Ko, F.M. Maggi, M. Montali, A. Rivkin, S. Winkler.
   Approximating Multi-perspective Trace Alignment Using Trace Encodings
   In BPM 2023, LNCS 14159, pp. 74-91. doi: 10.1007/978-3-031-41620-0_5
4. P. Felli, M. Montali, F. Patrizi, and S. Winkler.
   Monitoring Arithmetic Temporal Properties on Finite Traces
   AAAI 2023, AAAI Press 2023, pp. 6346-6354. doi: 10.1609/aaai.v37i5.25781 (long version available).
5. P. Felli, M. Montali, and S. Winkler.
   CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic
   In IJCAR 2022, 2022, LNCS 13385, pp. 36-56. doi: 10.1007/978-3-031-10769-6_4
6. P. Felli, M. Montali, and S. Winkler.
   Soundness of Data-Aware Processes with Arithmetic Conditions
   In CAiSE 2022, 2022, LNCS 13295, pp. 389-406. doi: 10.1007/978-3-031-07472-1_23
7. P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler.
   Conformance Checking with Uncertainty via SMT
   In BPM 2022, 2022, LNCS 13420, pp. 199-216. doi: 10.1007/978-3-031-16103-2_15
8. P. Felli, M. Montali, and S. Winkler.
   Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic.
   In AAAI 2022, 2022, pp. 5642-5650. doi: 10.1609/aaai.v36i5.20505 (long version available)
9. P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler.
   CoCoMoT: Conformance Checking of Multi-perspective Processes via SMT
   In BPM 2021, 2021, LNCS 12875, pp. 217-234. Best paper award. doi: 10.1007/978-3-030-85469-0_15
10. S. Winkler and G. Moser.
    Runtime Complexity Analysis of Logically Constrained Rewriting
    In LOPSTR 2020, 2020, LNCS 12561, pp. 37-55. doi: 10.1007/978-3-030-68446-4_2
11. M.P. Bonacina and S. Winkler.
    SGGS Decision Procedures
    In 10th IJCAR, LNCS 12166, pp. 356-374, 2020. Nominated for best paper award. ©Springer
12. C. Sternagel and S. Winkler.
    Certified equational reasoning via ordered completion
    In 27th CADE, LNCS 11716, pp. 508-525, 2019. ©Springer
13. S. Winkler.
    Extending maximal completion
    In FSCD 2019, LIPIcs 131, pp. 3:1-3:15, 2019. ©Creative Commons
14. S. Winkler and A. Middeldorp
    Tools in Term Rewriting for Education
    In ThEdu 2019, EPTCS 313, pp. 54-72, 2019. ©Creative Commons
15. N. Nishida and S. Winkler
    Loop Detection by Logically Constrained Term Rewriting
    In VSTTE 2018, LNCS 11294, pp. 309-321, 2018. ©Springer
16. S. Winkler and A. Middeldorp
    Completion for Logically Constrained Rewriting
    In FSCD 2018, LIPIcs 109, pp. 30:1-30:18, 2018. ©Creative Commons
17. S. Winkler and G. Moser
    MaedMax: A Maximal Ordered Completion Tool
    In IJCAR 2018, LNCS 10900, pp. 472-480, 2018. ©Springer-Verlag
18. 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
19. S. Winkler and R. Thiemann
    Formalizing Soundness and Completeness of Unravelings
    In FroCoS 2015, LNCS 9322, pp. 239-255, 2018. ©Springer-Verlag
20. 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
21. T. Sternagel, S. Winkler, and H. Zankl
    Recording Completion for Certificates in Equational Reasoning
    In CPP 2015, ACM, pp. 41-47, 2015
22. 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.
23. A. Yamada, S. Winkler, N. Hirokawa, and A. Middeldorp
    AC-KBO Revisited (report version)
    In 12th FLOPS, LNCS 8475, pp. 319-335, 2014.
24. S. Winkler and A. Middeldorp
    Normalized Completion Revisited
    In 24th RTA, LIPIcs 21, pp 319-334, 2013.
25. 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.
26. S. Winkler, H. Zankl, and A. Middeldorp
    Ordinals and Knuth-Bendix Orders
    In LPAR-18, LNCS 7180, pp 420-434, 2012. ©Springer-Verlag
27. S. Winkler and A. Middeldorp
    AC Completion with Termination Tools
    In CADE 23, LNCS (LNAI) 6803, pp 492-498, 2011. ©Springer-Verlag
28. S. Winkler and A. Middeldorp
    Termination Tools in Ordered Completion
    In IJCAR 2010, LNCS (LNAI) 6173, pp. 518-532, 2010. ©Springer-Verlag
29. S. Winkler, H. Sato, A. Middeldorp, and M. Kurihara
    Optimizing mkbTT (System Description)
    In 21st RTA, LIPIcs 13, pp 373-384, 2010. Creative-Commons
30. 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. M. Montali, and S. Winkler
   Equivalence of Data Petri Nets with Arithmetic
   In FM-BPM, 2023.
2. P. Felli, M. Montali, and S. Winkler
   Reasoning and Verification with Data Petri Nets
   In PMAI@IJCAI, 2022.
3. M. P. Bonacina and S. Winkler
   On SGGS and Horn Clauses
   In Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning (PAAR 2022), CEUR-WS 3201, 2022.
4. M. Suda and S. Winkler
   Learning Strategy Design: First Lessons
   In Proceedings of the 4th Conference on Artificial Intelligence in Theorem Proving (AITP 2020), pp 79-81, 2020.
S. Winkler and G. Moser
Smarter Features, Simpler Learning?
In Proceedings of the 2nd Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019), 2019.
5. C. Sternagel and S. Winkler
   Certified Ordered Completion
   In Proceedings of the 7th International Workshop on Confluence (IWC 2018), pp 41-45, 2018.
6. S. Winkler
   A Ground Joinability Criterion for Ordered Completion
   In Proceedings of the 6th International Workshop on Confluence (IWC 2017), pp 45-50, 2017.
7. 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.
8. 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.
9. 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.
10. 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
11. 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.