I am working on making the design process of correct-by-construction computational systems more efficient. My focus areas are:
September 2024: I'll be at the TAP 2024 and FM 2024 conferences. The content of the invited talk at TAP is can be read up in the respective paper in the proceedings.
May 2023: My Volkswagenstiftung Momentum endeavor got funded.
April 2023: Waiting for the first Temporal Logic Runtime Monitoring Circuit to be manufactured as part of the Open-MPW-6 program. Looking forward, though!
December 2022: A video containing a talk on the Natural Colors of Infinite Words has been added. It presents the results published in a paper accepted at FSTTCS 2022.
September 2022: A video containing a Gentle Introduction to Reactive Synthesis has been added.
July 2020: Paper presented at SAT 2020, Paper accepted at FMCAD 2020.
October 2019: I will participate in the Shonan Seminar on Software Engineering for Machine Learning Systems this month.
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.