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 learning-based verification and synthesis of complex systems. On top of that, I work on logics as well as on the question of how the design and specification of systems can be improved by machine learning.

Recently, I became interested in exploring how immersive visualization technology (VR) can be used for designing and analyzing concurrent systems.

Recent Talks and Tutorials

  • 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

Tools

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

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

    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

    Horn-ICE is an extension of the ICE tool suite to verification conditions in form of Constrainted Horn clauses. An interface to the SeaHorn verification framework is currently under development.

Artifacts

  • Invariant Synthesis for Incomplete Verification Engines

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

Teaching

  • Advanced Automata Theory (graduate course)

  • Concurrency Theory (graduate course)

  • 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

  • Organizer of the upcoming seminar on Logic and Learning (summer 2019)

Program Committee Member

Publications

See my DBLP entry for a complete list.

Under Review

  • Evrostos: The rLTL Verifier

    T. Anevlavis, D. Neider, M. Phillipe, P. Tabuada
  • Learning-Based Synthesis of Safety Controllers

    D. Neider, O. Markgraf
  • Robust, Expressive, and Quantitative Linear Temporal Logicspdf

    D. Neider, A. Weinert, M. Zimmermann
  • Robust Monitoring of Linear Temporal Properties pdf

    D. Neider, M. Schwenger, P. Tabuada, A. Weinert, and M. Zimmermann

Conferences

  • 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

    T. Anevlavis, M. Philippe, D. Neider, and P. Tabuada
    In proceedings of IEEE Conference on Decision and Control (CDC), to appear
  • 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, 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