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 automated tools for the design, the construction, and the analysis of intelligent systems.

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

  • Verification of learning systems: automatically proving correctness properties (e.g., robustness) of learning systems.
  • Explanability of artificial intelligence: generating provably correct explanations for the decision making of intelligent systems.
  • Intelligent formal methods: tools that learn correctness and termination proofs for a wide range of systems, including hardware, software, and cyber-physical systems.
  • 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.

Our projects often 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.

  • QUGA

    QUGA (short for Quality Guarantees for Autoencoders) is a tool for the deductive verification of deep auto encoders. The sources are hosted on GitHub.

  • RESCOT

    RESCOT is a C++ tool (with a small Matlab interface) to synthesize resilient controllers for (possibly perturbed) nonlinear control systems with respect to safety and reachability specifications. The sources are available on BitBucket.

  • Traces2LTL

    Traces2LTL is a collection of algorithms for learning LTL formulas from labeled, infinite words (see the flie web demo). 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

Projects

I am principal investigator in the following projects.

LeaRNNify

The DAAD-supported project LeaRNNify is at the interface of formal methods and artificial intelligence. Its aim is to bring together two different kinds of algorithmic learning, namely grammatical inference and learning of neural networks.

More precisely, we promote the use of recurrent neural networks (RNNs) in the process of verifying reactive systems, which until now has been reserved for grammatical inference. On the other hand, grammatical inference is finding its way into the field of classical machine learning. In fact, our second goal is to use automata-learning techniques to enhance the verification, explainability, and interpretability of machine-learning algorithms and, in particular, RNNs.

Also visit our project website.

Temporal Logic Sketching

The goal of the DFG-funded project Temporal Logic Sketching is to develop computer-aided methods to assist engineers in writing formal specifications. To this end, the project combines inductive and deductive techniques from the areas of machine learning, artificial intelligence, and logic. As a byproduct, the project also investigates explainable machine learning, specifically learning of human-interpretable models.

Recent Talks and Tutorials

  • Neuro-Symbolic Verification of Deep neural Networks. IJCAI, July 2022, Vienna, Austria
  • Safety and Explainability of Learning Systems. Invited talk, December 2021, Technical University of Dortmund, Germany
  • (Horn-)ICE Learning: An Inductive Approach to Deductive Software Verification. Invited talk, June 2021, RWTH Aachen University, Germany
  • Logic and Learning: Formal Guarantees for Trustworthy Intelligent Systems. Invited talk, November 2020, University of Oldenburg, Germany
  • Learning Correctness Proofs of Software. Invited talk, January 2020, University of Liverpool, UK
  • Combining Deductive and Inductive Reasoning in Formal Methods. Invited talk, October 2019, University of California, Los Angeles, USA
  • 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

Professional Activities

Dagstuhl Seminars

Publications

See my DBLP and Google Scholar entries for a complete list.

Under Submission

  • Specification Sketching for Linear Temporal Logic pdf

    S. Lutz, D. Neider, and R. Roy

  • A Formal Language Approach to Explaining RNNs pdf

    B. Gosh and D. Neider

  • Probably Approximately Correct Explanations of Machine Learning Models via Syntax-Guided Synthesis pdf

    D. Neider and B. Ghosh

Conferences

  • Learning Interpretable Temporal Properties from Positive Examples Only pdf

    R. Roy, J.-R. Gaglione, N. Baharisangari, D. Neider, Z. Xu, Zhe, and U. Topcu
    In proceedings of AAAI Conference on Artificial Intelligence (AAAI), to appear

  • Analyzing Robustness of Angluin's L* Algorithm in Presence of Noise pdf

    I. Khmelnitsky, S. Haddad, L. Ye, B. Barbot, B. Bollig, M. Leucker, D. Neider, and R. Roy
    In proceedings of International Symposium on Games, Automata, Logics and Formal Verification (GandALF), 2022

  • Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime pdf

    S. P. Nayak, D. Neider, and M. Zimmermann
    In proceedings of International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2022

  • Neuro-Symbolic Verification of Deep Neural Networks pdf

    X. Xie, K. Kersting, and D. Neider
    In proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2022

  • A Survey of Model Learning Techniques for Recurrent Neural Networks pdf

    B. Bollig, M. Leucker, and D. Neider
    In A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, 2022

  • Learning to Break Deep Perceptual Hashing: The Use Case NeuralHash pdf

    L. Struppek, D. Hintersdorf, D. Neider, and K. Kersting
    In proceedings of ACM Conference on Fairness, Accountability, and Transparency (FAccT), 2022

  • Reinforcement Learning with Stochastic Reward Machines pdf

    J. Corazza, I. Gavran, and D. Neider
    In proceedings of AAAI Conference on Artificial Intelligence (AAAI), 2022

  • Robust Computation Tree Logic pdf

    S. P. Nayak, D. Neider, R. Roy, and M. Zimmermann
    In proceedings of NASA Formal Methods Symposium (NFM), 2022

  • Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic pdf

    R. Raha, R. Roy, N. Fijalkow, and D. Neider
    In proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2022

  • Property-Directed Verification and Robustness Certification of Recurrent Neural Networks pdf

    B. Barbot, B. Bollig, A. Finkel, S. Haddad, M. Leucker, D. Neider, I. Khmelnitsky, R. Roy, L. Ye, and X. Xie
    In proceedings of International Symposium on Automated Technology for Verification and Analysis (ATVA), 2021

  • Learning Linear Temporal Properties from Noisy Data: A MaxSAT Approach pdf

    J.-R. Gaglione, D. Neider, R. Roy, U. Topcu, and Z. Xu
    In proceedings of International Symposium on Automated Technology for Verification and Analysis (ATVA), 2021

  • Uncertainty-Aware Signal Temporal Logic Inference pdf

    N. Baharisangari, J.-R. Gaglione, D. Neider, U. Topcu, and Z. Xu
    In proceedings of International Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2021

  • Extracting Context-Free Grammars from Recurrent Neural Networks using Tree-Automata Learning and A* Search pdf video

    B. Barbot, B. Bollig, A. Finkel, S. Haddad, M. Leucker, D. Neider, I. Khmelnitsky, R. Roy, and L. Ye
    In proceedings of International Conference on Grammatical Inference (ICGI), 2021

  • Active Finite Reward Automaton Inference and Reinforcement Learning Using Queries and Counterexamples pdf

    Z. Xu, B. Wu, A. Ojha, D. Neider, and U. Topcu
    In proceedings of International Cross Domain Conference for Machine Learning & Knowledge Extraction (CD-MAKE), 2021

  • Advice-Guided Reinforcement Learning in a Non-Markovian Environment pdf video

    J.-R. Gaglione, I. Gavran, D. Neider, U. Topcu, B. Wu, and Z. Xu
    In proceedings of AAAI Conference on Artificial Intelligence (AAAI), 2021

  • Quality Guarantees for Autoencoders via Unsupervised Adversarial Attacks pdf video

    B. Böing, R. Roy, E. Müller, and D. Neider
    In proceedings of European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases (ECML-PKDD), 2020

  • Learning Interpretable Models in the Property Specification Language pdf

    R. Roy, D. Fisman, and D. Neider
    In proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2020

  • Learning Temporal Properties in LTL ∩ ACTL from Positive Examples Only pdf video

    I. Gavran, R. Ehlers, and D. Neider
    In proceedings of Conferences on the Theory and Applications of Formal Methods in Hardware and System Verification (FMCAD), 2020

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

    Z. Xu, I. Gavran, Y. Ahmad, R. Majumdar, D. Neider, U. Topcu, and B. Wu
    In proceedings of International Conference on Automated Planning and Scheduling (ICAPS), 2020

  • Optimally Resilient Strategies in Pushdown Safety Games pdf video

    D. Neider, P. Totzke, and M. Zimmermann
    In proceedings of International Symposium on Mathematical Foundations of Computer Science (MFCS), 2020

  • Parameterized Synthesis with Safety Properties pdf video

    C.-D. Hong, M. Najib, A. Lin, O. Markgraf, and D. Neider
    In proceedings of Asian Symposium on Programming Languages and Systems (APLAS), 2020

  • Resilient Abstraction-Based Controller Design pdf video

    S. Samuel, K. Mallik, A.-K. Schmuck, and D. Neider
    In proceedings of IEEE Conference on Decision and Control (CDC), 2020

  • From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics pdf

    C. Mascle, D. Neider, M. Schwenger, P. Tabuada, A. Weinert, and M. Zimmermann
    In proceedings of ACM International Conference on Hybrid Systems: Computation and Control (HSCC), 2020

  • 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

  • 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

  • Benchmarks for Automata Learning and Conformance Testing pdf

    D. Neider, R. Smetsers, F. W. Vaandrager, H. Kuppens
    In Models, Mindsets, Meta - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday, 2018

  • Horn-ICE Learning for Synthesizing Invariants and Contracts pdf video

    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

  • Invariant Synthesis for Incomplete Verification Engines pdf

    D. Neider, P. Madhusudan, P. Garg, S. Saha, D. Park
    In proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 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 video

    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

  • Learning Automata for Streaming XML Documents

    D. Neider
    In Informatiktage 2008 - Fachwissenschaftlicher Informatik-Kongress, 2008

  • MediSign - Secure Pharmaceutic Distribution

    M. Möllers, E. Müller, D. Neider, L. Seweryn
    In Informatiktage 2006 - Fachwissenschaftlicher Informatik-Kongress, 2006

Journals

  • Property-Directed Verification and Robustness Certification of Recurrent Neural Networks pdf

    I. Khmelnitsky, D. Neider, R. Roy, X. Xie, B. Barbot, B. Bollig, A. Finkel, S. Haddad, M. Leucker, and L. Ye
    In International Journal on Software Tools for Technology Transfer, 2022

  • MaxSAT-based Temporal Logic Inference from Noisy Data pdf

    J.-R. Gaglione, D. Neider, R. Roy, U. Topcu, and Z. Xu
    In Innovations in Systems and Software Engineering 18, 2022

  • Being Correct is Not Enough: Efficient Verification Using Robust Linear Temporal Logic pdf

    T. Anevlavis, M. Philippe, D. Neider, and P. Tabuada
    In Transactions on Computational Logic 23(2), 2022

  • Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free (Extended Version) pdf

    D. Neider, A. Weinert, and M. Zimmermann
    In Information and Computation 285(Part B), 2022

  • A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines pdf

    D. Neider, P. Madhusudan, S. Saha, P. Garg, D. Park
    In Journal of Automated Reasoning 64(7), 2020

  • Synthesizing optimally resilient controllers pdf

    D. Neider, A. Weinert, M. Zimmermann
    In Acta Informatica 57(1-2), 2020

  • 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

Posters and Workshop Papers

  • Expanding the Horizon of Linear Temporal Logic Inference for Explainability pdf

    D. Neider and R. Roy
    In IEEE International Requirements Engineering Conference Workshops (RE), 2022

  • QUGA - Quality Guarantees for Autoencoders pdf

    B. Böing, R. Roy, D. Neider, and E. Müller
    In Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis (OVERLAY) @ GandALF, 2021

  • Adaptive Strategies for rLTL Games pdf

    S. P. Nayak, D. Neider, and M. Zimmermann
    In International Conference on Hybrid Systems: Computation and Control (HSCC), 2021

  • Resilient Abstraction-Based Controller Design pdf video

    S. Samuel, K. Mallik, A.-K. Schmuck, and D. Neider
    In International Conference on Hybrid Systems: Computation and Control (HSCC), 2020

  • Development of libALF

    D. Neider
    In Entwicklung und Evolution von Forschungssoftware: Tagungsband des Workshops, 2011

Dagstuhl Reports

  • Logic and Learning (Dagstuhl Seminar 19361) pdf

    M. Benedikt, K. Kersting, P. G. Kolaitis, and D. Neider
    In Dagstuhl Reports 9(9), 2019

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