Rüdiger Ehlers


Rüdiger Ehlers
Professor for Embedded Systems
Clausthal University of Technology
Institute for Software and Systems Engineering
Arnold-Sommerfeld-Straße 1
38678 Clausthal-Zellerfeld

Phone (at TU Clausthal): +49 5323 / 72-7148

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 (old) research group.


  • June 2019: Papers accepted at the ATVA 2019 and FM 2019 conferences.

  • May 2019: I am now an Associate Professor for Embedded Systems at Clausthal University of Technology. A press release with the news in German can he found here.

  • January 2019: I am a member of the program committees of the HSCC 2019 and EMSOFT 2019 conferences.

  • July 2018: Papers accepted at the ATVA 2018 and CDC 2018 conferences.

  • April 2018: The paper “Approximately Propagation Complete and Conflict Propagating Constraint Encodings” by Francisco Palau Romero and me has been accepted at the SAT 2018 conference.

  • January 2018: Two papers co-authored by me were accepted at AAAI 2018 and ACC 2018. They can be downloaded here (AAAI) and here (ACC).

    You can download the authors' version of the work. It is posted here for your personal use. Not for redistribution.

  • December 2017: I will be speaking on the 1st Workshop on Probabilistic Reasoning and Formal Methods to be held at IIT Kanpur, India, on the 11th of December. My talk will provide a non-classical perspective on computing control policies for enforcing omega-regular control objectives in Markov decision processes.

  • 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 published version of the paper can be downloaded here.

    The full version of the paper (with proofs) is available on ArXiV/CoRR.

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