Logic, Interactive Theorem Proving, Automated Reasoning, Functional Programming

• SMT-solving (e.g. conflict-driven satisfiability)
• Type systems, type theory, models of proofs and programs (e.g. realisability)
• Combination of logic-based AI and machine learning (e.g. verification of neural nets, learning for proof-search guidance)
• Correct-by-construction software, formal specifications within software development