Archived Website: I moved to the Hebrew University of Jerusalem. This page is no longer maintained. Visit the previous link for the new webpage.
I am a postdoctoral student at the Hebrew University of Jerusalem as a member of Orna Kupferman’s group. I am currently holding a DFG fellowship. I received my doctoral degree at the Technical University of Munich under the supervision of Javier Esparza in 2019. A complete CV is available upon request.
My research lies at the intersection of formal methods and theoretical computer science. I study the foundations of algorithmic verification with the intended goal of allowing for the development of more reliable software and systems. My interests include automata theory, logic, formal verification, model checking and synthesis of reactive systems, computational complexity theory, theorem provers, and verification tools.
Contact me: salomon (dot) (lastname) (at) mail (dot) huji (dot) ac (dot) il
Find me on: DBLP, Google Scholar, ORCID, and GitHub
Orna Kupferman, Nir Lavee, Salomon Sickert
Certifying DFA Bounds for Recognition and Separation
Innovations in Systems and Software Engineering (2022): bibtex / view
Javier Esparza, Jan Křetínský, Salomon Sickert
A Unified Translation of Linear Temporal Logic to ω-Automata
Journal of the ACM (2020): bibtex / view
Michael Luttenberger, Philipp J. Meyer, Salomon Sickert
Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games
Acta Informatica (2020): bibtex / view / full version
Javier Esparza, Jan Křetínský, Salomon Sickert
From LTL to deterministic automata - A safraless compositional approach
FMSD (2016): bibtex / view / full version
Nikola Beneš, Jan Křetínský, Kim G. Larsen, Mikael H. Møller, Salomon Sickert, Jiří Srba
Refinement checking on parametric modal transition systems
Acta Informatica (2015): bibtex / view
Udi Boker, Karoliina Lehtinen, Salomon Sickert
On the Translation of Automata to Linear Temporal Logic
FoSSaCS (2022): bibtex / view / full version
Antonio Casares, Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin, Salomon Sickert
Practical Applications of the Alternating Cycle Decomposition
TACAS (2022): bibtex / view / full version
Orna Kupferman, Salomon Sickert
Certifying Inexpressibility
FoSSaCS (2021): bibtex / view / full version
Orna Kupferman, Nir Lavee, Salomon Sickert
Certifying DFA Bounds for Recognition and Separation
ATVA (2021): bibtex / view / full version
Philipp J. Meyer, Salomon Sickert
Modernising Strix
SYNT Workshop (2021): bibtex / full version
Remco Abraham, Tom van Dijk, Salomon Sickert
Almost-Symbolic Synthesis via ∆2-Normalisation for Linear Temporal Logic
SYNT Workshop (2021): bibtex / full version
Salomon Sickert, Javier Esparza
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
LICS (2020): bibtex / view / full version / λ formalisation / Java implementation / recording / online demo
Julian Brunner, Benedikt Seidl, Salomon Sickert
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata
ITP (2019): bibtex / view / λ formalisation
Jan Křetínský, Tobias Meggendorfer, Salomon Sickert
Owl: A Library for ω-Words, Automata, and LTL
ATVA (2018): bibtex / view / full version
Javier Esparza, Jan Křetínský, Salomon Sickert
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
LICS (2018): bibtex / view / full version
Philipp Meyer, Salomon Sickert, Michael Luttenberger
Strix: Explicit Reactive Synthesis Strikes Back!
CAV (2018): bibtex / view / full version
Jan Křetínský, Tobias Meggendorfer, Salomon Sickert, Christopher Ziegler
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton
CAV (2018): bibtex / view / full version
Javier Esparza, Jan Křetínský, Jean-Francois Raskin, Salomon Sickert
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
TACAS (2017): bibtex / view / full version
David Müller, Salomon Sickert
LTL to Deterministic Emerson-Lei Automata
GandALF (2017): bibtex / view
Salomon Sickert, Jan Křetínský
MoChiBA: Probabilistic LTL Model Checking using limit-deterministic Büchi Automata
ATVA (2016): bibtex / view / full version
Salomon Sickert, Javier Esparza, Stefan Jaax, Jan Křetínský
Limit-Deterministic Büchi Automata for Linear Temporal Logic
CAV (2016): bibtex / view / full version
Jan Křetínský, Salomon Sickert
MoTraS: A Tool for Modal Transition Systems and Their Extensions
ATVA (2013): bibtex / view
Jan Křetínský, Salomon Sickert
On Refinements of Boolean and Parametric Modal Transition Systems
ICTAC (2013): bibtex / view
Salomon Sickert
Deterministic ω-Automata for LTL-Fragments: A Mechanically Verified Construction
M.Sc. Thesis (2014)
Salomon Sickert
Refinement Algorithms for Parametric Modal Transition Systems
B.Sc. Thesis (2012)
Salomon Sickert
An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation
Archive of Formal Proofs (2020): bibtex / view
Benedikt Seidl, Salomon Sickert
A Compositional and Unified Translation of LTL into ω-Automata
Archive of Formal Proofs (2019): bibtex / view
Salomon Sickert
Linear Temporal Logic
Archive of Formal Proofs (2016): bibtex / view
Salomon Sickert
Converting Linear Temporal Logic to Deterministic (Generalised) Rabin Automata
Archive of Formal Proofs (2015): bibtex / view
Owl is a Java 11 tool collection and library for ω-words, ω-automata and linear temporal logic. It provides a wide range of algorithms for automata and LTL. The project is hosted at owl.model.in.tum.de. Previously published tools such as ltldpa and ltl2ldba are now shipped with Owl.
Strix is a reactive synthesis tool based on Owl. The project is hosted at strix.model.in.tum.de.
A prototype using ltl2ldba from Owl for quantitative model checking of MDPs (Markov decision process). Based on the PRISM model checker. The project is hosted here.
A tool for modal transition systems and their extensions supporting modal refinement checking and provides GUI for drawing. All information for this project is located at this website.
A tool constructing deterministic (generalised) Rabin Automata for LTL (Linear Temporal Logic). The implementation is extracted from the mechanically verified formalisation. The algorithm is compositional, safra-less, and yields small automata. It is closely related to Rabinizer 3, since both tools implement the same algorithm and inspire each other. The only major difference is that LTL_to_DRA is formally verified, while Rabinizer 3 provides more features and has shorter running times. More information can be found here.