Portrait

Contact

+49 631 93038529
Paul-Ehrlich-Str. 26
Room 316
67663 Kaiserslautern
Germany

Research

My research interests broadly lie in the intersection of machine learning and formal methods. I am especially interested in combining inductive techniques from the area of machine learning and symbolic techniques from the area of logic. The goal of my group is to build intelligent, automated tools for the design, the construction, and the analysis of hardware, software, and cyber-physical systems.

My group is working on a number of topics, including:

  • Intelligent formal methods: tools that learn correctness and termination proofs for software.
  • Learning-based synthesis: automatically generating reactive systems and program code from logical specifications and examples.
  • Specification learning/recommendation: learning-based methods that assist humans in writing formal specifications.
  • Incorporating automata learning and symbolic reasoning in reinforcement learning, inverse reinforcement learning, and transfer learning.
  • Learning theory: developing principled ways to combine learning and symbolic reasoning.

Some of our projects also extend into theoretical computer science, specifically to automata theory, game theory, and logic.

You can try some of the tools we have developed online:

Tools

As a byproduct of my research, I have developed and contributed to a number of tools:

  • Alchemist-CS/DT

    Alchemist-CS/DT is a synthesizer for piece-wise linear integer arithmetic expressions from SyGuS specifications, which combines logical constraint solving with decision tree learning.
  • Evrostos: The rLTL Verifier

    Evrostos is an efficient, NuSMV-based model checker for rLTL properties. The sources are hosted on GitHub.
  • ICE Verification Toolkit

    ICE is a fully automated program verifier, which extends Microsoft Boogie with various learning-based methods for automatic invariant generation. It has won the invariant synthesis track of the Syntax-Guided Synthesis Competition in 2015 and 2016.
  • Horn-ICE Verification Toolkit

    Horn-ICE is an extension of the ICE tool suite that supports the verification of recursive and concurrent programs. It it also able to synthesize solutions for Constrained Horn clauses. The sources are hosted on GitHub.
  • libalf

    Libalf is a fast, open-source library for learning finite state machines. It implements a wide range of popular active and passive learning algorithms for deterministic and nondeterministic finite automata as well as Moore Machines. The sources are available on GitHub.
  • Traces2LTL

    Traces2LTL is a collection of algorithms that learn LTL formulas from classified, infinite words that combines SAT solving with learning of decision trees. The sources are hosted on GitHub.

Artifacts

  • Horn-ICE Learning for Synthesizing Invariants and Contracts

    Tools and benchmarks developed for the paper Horn-ICE Learning for Synthesizing Invariants and Contracts
  • Invariant Synthesis for Incomplete Verification Engines

    Tools and benchmarks developed for the paper Invariant Synthesis for Incomplete Verification Engines

Recent Talks and Tutorials

  • Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants. SAS, October 2019, Porto, Portugal
  • Deductive Verification, the Inductive Way. Invited tutorial at the ForMaL Spring School on Formal Methods and Machine Learning, June 2019, ENS Paris-Saclay, France
  • Formal Verification Meets Machine Learning. Invited talk, March 2019, University of Bochum, Germany
  • Learning Linear Temporal Properties. Invited talk, Complexity, Algorithms, Automata and Logic Meet, January 2019, Chennai Mathematical Institute, India
  • Horn-ICE Learning for Synthesizing Invariants and Contracts. OOPSLA, November 2018, Boston, MA, USA
  • Learning Linear Temporal Properties. Invited talk, Highlights of Logic, Games and Automata, September 2018, Berlin, Germany
  • A Tutorial on Automata Learning. Invited tutorial at MOVEP '18 Summer School, July 2018, ENS Paris-Saclay, France
  • Machine Learning Meets Formal Methods. Invited talk, June 2018, Saarland University, Germany
  • Invariant Synthesis for Incomplete Verification Engines. TACAS, April 2018, Thessaloniki, Greece
  • Logic and Learning. Invited talk, February 2018, University of Kaiserslautern, Germany
  • Solving Safety Games over Infinite Graphs. GI Theorietage, September 2017, Bonn, Germany
  • Robust Linear Temporal Logic. DARS (at CAV), July 2017, Heidelberg, Germany
  • ICE Learning: An Overview. LiVe (at ETAPS), April 2017, Uppsala, Sweden
  • Synthesizing Invariants via Iterative Learning of Decision Trees. LDWA, September 2016, Hasso-Plattner-Institut, Potsdam, Germany
  • Robust Linear Temporal Logic. CSL, August 2016, Marseille, France
  • Synthesizing Piece-Wise Functions by Learning Classifiers. Invited talk, July 2016, Technische Universität Dortmund, Germany
  • Learning-Based Synthesis. Invited Talk, May 2016, Universität Paderborn, Germany
  • An Automaton Learning Approach to Solving Safety Games over Infinite Graphs. TACAS, April 2016, Eindhoven, Netherlands
  • Synthesizing Piece-Wise Functions by Learning Classifiers. TACAS, April 2016, Eindhoven, Netherlands
  • Robustness and Linear Temporal Logic. Invited talk, Januar 2016, Technische Universität München, Germany
  • Robust LTL, ExCAPE Meeting, June 2015, Massachusetts Institute of Technology, Cambridge, MA, USA
  • An Introduction to Automata Learning. Invited talk, August 2014, University of Pennsylvania, Philadelphia, PA, USA

Teaching

  • Advanced Automata Theory (graduate course)

  • Concurrency Theory (graduate course)

  • Program Analysis (graduate course)

  • Applied Verification Lab (project)

  • Logic and Verification Seminar

  • Bachelor/Master Projects and Theses

    I am supervising Bachelor and Master theses centering around machine learning in verification and synthesis. Should you be looking for a thesis or project in these areas, please contact me for further information.

Professional Activities

Dagstuhl Seminars

Program Committee Member

Publications

See my DBLP entry for a complete list.

Under Submission

  • Joint Inference of Reward Machines and Policies for Reinforcement Learning pdf

    Z. Xu, I. Gavran, Y. Ahmad, R. Majumdar, D. Neider, U. Topcu, B. Wu
  • From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics pdf

    C. Mascle, D. Neider, M. Schwenger, P. Tabuada, A. Weinert, and M. Zimmermann
  • Optimally Resilient Strategies in Pushdown Safety Games

    D. Neider, P. Totzke, and M. Zimmermann

Conferences

  • Learning-Based Synthesis of Safety Controllers pdf

    D. Neider and O. Markgraf
    In proceedings of Conferences on the Theory and Applications of Formal Methods in Hardware and System Verification (FMCAD), 2019 (to appear)
  • Sorcar: Efficient Algorithms for Learning Small Conjunctive Invariants pdf

    D. Neider, S. Saha, P. Garg, and P. Madhusudan
    In proceedings of International Static Analysis Symposium (SAS), 2019
  • Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free pdf

    D. Neider, A. Weinert, and M. Zimmermann
    In proceedings of International Symposium on International Symposium on Games, Automata, Logics and Formal Verification (GandALF), 2019
  • Evrostos: The rLTL Verifier pdf

    T. Anevlavis, D. Neider, M. Phillipe, and P. Tabuada
    In proceedings of ACM International Conference on Hybrid Systems: Computation and Control (HSCC), 2019
  • Horn-ICE Learning for Synthesizing Invariants and Contracts pdf

    D. D'Souza, P. Ezudheen, P. Garg, P. Madhusudan and D. Neider
    2018 conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2018
  • Learning Linear Temporal Properties pdf

    D. Neider and I. Gavran
    In proceedings of Conferences on the Theory and Applications of Formal Methods in Hardware and System Verification (FMCAD), 2018
  • Verifying rLTL Formulas: Now Faster Than Ever Before! pdf

    T. Anevlavis, M. Philippe, D. Neider, and P. Tabuada
    In proceedings of IEEE Conference on Decision and Control (CDC), 2018
  • Synthesizing Optimally Resilient Controllers pdf

    D. Neider, A. Weinert, M. Zimmermann
    In proceedings of EACSL Annual Conference on Computer Science Logic (CSL), 2018
  • Synthesis of Safety Controllers Robust to Unmodeled Intermittent Disturbances pdf

    E. Dallal, D. Neider, P. Tabuada
    In proceedings of IEEE Conference on Decision and Control (CDC), 2016
  • Robust Linear Temporal Logic pdf

    P. Tabuada, D. Neider
    In proceedings of EACSL Annual Conference on Computer Science Logic (CSL), 2016
  • Learning Invariants Using Decision Trees and Implication Counterexamples pdf

    P. Garg, D. Neider, P. Madhusudan, D. Roth
    In proceedings of Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016
  • Abstract Learning Frameworks for Synthesis pdf

    C. Löding, P. Madhusudan, D. Neider
    In proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016
  • An Automaton Learning Approach to Solving Safety Games over Infinite Graphs pdf

    D. Neider, U. Topcu
    In proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016
  • Synthesizing Piece-Wise Functions by Learning Classifiers pdf

    D. Neider, S. Saha, P. Madhusudan
    In proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016
  • ICE: A Robust Framework for Learning Invariants pdf

    P. Garg, C. Löding, P. Madhusudan, D. Neider
    In proceedings of International Conference on Computer Aided Verification (CAV), 2014
  • Learning Universally Quantified Invariants of Linear Data Structures pdf

    P. Garg, C. Löding, P. Madhusudan, D. Neider
    In proceedings of International Conference on Computer Aided Verification (CAV), 2013
  • Regular Model Checking Using Solver Technologies and Automata Learning pdf

    D. Neider, N. Jansen
    In proceedings of International Symposium NASA Formal Methods (NFM), 2013
  • Computing Minimal Separating DFAs and Regular Invariants Using SAT and SMT Solvers pdf

    D. Neider
    In proceedings of International Symposium on Automated Technology for Verification and Analysis (ATVA), 2012
  • Learning Minimal Deterministic Automata from Inexperienced Teachers pdf

    M. Leucker, D. Neider
    In proceedings of International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2012
  • Down the Borel Hierarchy: Solving Muller Games via Safety Games pdf

    D. Neider, R. Rabinovich, M. Zimmermann
    In proceedings of International Symposium on International Symposium on Games, Automata, Logics and Formal Verification (GandALF), 2012
  • Small Strategies for Safety Games pdf

    D. Neider
    In proceedings of International Symposium on Automated Technology for Verification and Analysis (ATVA), 2011
  • libalf: The Automata Learning Framework pdf

    B. Bollig, J.-P. Katoen, C. Kern, M. Leucker, D. Neider, D. Piegdon
    In proceedings of International Conference on Computer Aided Verification (CAV), 2010
  • Reachability Games on Automatic Graphs pdf

    D. Neider
    In proceedings of International Conference on Implementation and Application of Automata (CIAA), 2010

Journals

  • Compositional Synthesis of Piece-wise Functions by Learning Classifiers pdf

    D. Neider, S. Saha, P. Madhusudan
    In Transactions on Computational Logic 19(2), Article No. 10, 2018
  • Quantified Data Automata for Linear Data Structures: a Register Automaton Model with Applications to Learning Invariants of Programs Manipulating Arrays and Lists pdf

    P.Garg, C. Löding, P. Madhusudan, D. Neider
    In Formal Methods in System Design 47(1), 2015
  • Down the Borel Hierarchy: Solving Muller games via Safety Games pdf

    D. Neider, R. Rabinovich, M. Zimmermann
    In Theor. Comput. Sci. 560, 2014
  • Lernverfahren für Automaten über linearisierten XML-Dokumenten pdf

    D. Neider
    In Informatik Spektrum 32(3), 2009

Technical Reports

  • Learning Visibly One-Counter Automata in Polynomial Time pdf

    D. Neider, C. Löding
    In Technical report AIB-2010-02, RWTH Aachen, 2010

Thesis

  • Applications of Automata Learning in Verification and Synthesis pdf

    D. Neider
    RWTH Aachen University, 2014