Research

My former and current PhD students are given here.

• Dmitri Chubarov (Infinite-state model checking with integers)
• Shasha Feng (Advanced term indexing)
• Krystof Hoder (Efficient First-Order Theorem Proving)
• Mohammed Khazal Jaber (The design and implementation of UNIDOOR: the Deductive Object-Oriented Database System)
• Konstantin Korovin (Knuth-Bendix orders in automated deduction and term rewriting)
• Iman Narasamdya (Establishing program equivalence in translation validation for optimising compilers)
• Juan Antonio Navarro Perez (Encoding and solving problems in effectively propositional logic)
• Alexandre Riazanov (The design and implementation of Vampire)
• Andrei Tchaltsev (Self-validating compilation based on phase semantics)
• Lars Thalmann (Term-modal logics)
• Nestan Tsiskaridze (Satisfiability modulo theories)
• Margus Veanes (On simultaneous rigid E-unification)