Rüdiger Ehlers


Rüdiger Ehlers
Junior Research Group Leader for “Modelling of Technical Systems”
Department of Mathematics & Computer Science
University of Bremen
Bibliotheksstraße 1 / MZH Building, Room 1265
28259 Bremen

E-Mail Address: mail<current-4digit-year>@ruediger-ehlers.de

You can download my GnuPG/PGP key here.

Research Interests

I am working on making the design process of correct-by-construction computational systems more efficient. My focus areas are:

  • Reactive synthesis

  • Reasoning engines for logical problems

  • Verification of finite-state and infinite-state systems

  • Bridging the gap between formal methods and artificial intelligence

More information can be found on my research page and the web page of my research group.


  • October 2017: The paper “Symmetric Synthesis” by Bernd Finkbeiner and me was accepted at the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

    The full version of this paper (with proofs) is available on ArXiV/CoRR. The published version will appear in the LIPIcs proceedings series.

  • September 2017: A preprint of the paper Safe Reinforcement Learning via Shielding by Mohammed Alshiekh, Roderick Bloem, Bettina Könighofer, Scott Niekum, Ufuk Topcu, and me is now available on ArXiV. The paper shows how to perform safe reinforcement learning, i.e., how to enforce a temporal logic specification during the learning process of a cyber-physical system control strategy. The presented approach thus supports the use of machine learning for safety-critical control applications (e.g., in robotics).

  • August 2017: Two new short texts on Fulfilling Orders - An Algorithm Engineering Exercise and Deterministic Parity Automata – What Are They Good For? are now online. They are intended to be used as supplementary teaching material for SMT solving and automata theory, respectively.

  • July 2017: I will be giving a lecture on practical reactive synthesis on the Summer School on Formal Methods for Cyber-Physical Systems – Edition 2017: Automatic Synthesis of Controllers for Hybrid Systems, to be held in September 2017 in Verona, Italy.

  • July 2017: My paper “Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks” has been accepted at ATVA 2017. Its preprint can be read on ArXiV.

  • May 2017: The feed-forward neural network verification tool planet is now available for download from its Github page.

  • March 2017: The European Commission decided to fund the EU/H2020 Project SAFE-10-T, in which I serve as a PI.

  • February 2017: The slides from my “Towards Best-Effort Autonomy” talk at Dagstuhl seminar 17071 are available here.

  • August 2016: The German Science Foundation (DFG) accepted my project proposal on synthesizing program code for graphical user interfaces.

  • March 2016: The slugs tool paper has been accepted at CAV 2017. Its author-archived version also includes an appendix that serves as a gentle introduction to modelling specifications with slugs.

    Click here to download the author-archived version of the paper. Copyright by Springer Verlag. The original publication is available at www.springerlink.com

  • December 2015: You can now download C++ and Python implementations of my algorithm for enumerating all Pareto optima in a multi-dimensional discrete search space where only an oracle function is available that is known to be monotonous. The implementations are available here, and the preprint paper in which the algorithm is described is available here.