Salomon Sickert

PostDoc at HUJI

Short Biography

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 Information

Contact me: salomon (dot) (lastname) (at) mail (dot) huji (dot) ac (dot) il

Find me on: DBLP, Google Scholar, ORCID, and GitHub




Conferences & Workshops



Formal Proofs



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


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.

Rabinizer Verified (ltl2dra)

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.