Salomon Sickert

PostDoc at TUM and HUJI

About Me

I am a postdoctoral fellow at the Technical University of Munich and the Hebrew University of Jerusalem. I am a member of Javier Esparza’s group in Munich and a member of Orna Kupferman’s group in Jerusalem. 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. I received my Dr. rer. nat. (Ph.D.-equivalent) in 2019 from the Technical University of Munich.

Publications

Disseration

Journals

Conferences & Workshops

Theses

Formal Proofs

Tools

Owl

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

Strix is a reactive synthesis tool based on Owl. The project is hosted at strix.model.in.tum.de.

MoChiBA

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.

MoTraS

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