Comparing Unification Algorithms in First-Order Theorem Proving. - Krystof Hoder; Andrei Voronkov (KI, 2009)

Interpolation and Symbol Elimination in Vampire. - Krystof Hoder; Laura Kovács; Andrei Voronkov (IJCAR, 2010)

Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. - Josef Urban; Krystof Hoder; Andrei Voronkov (ICMS, 2010)

Sine Qua Non for Large Theory Reasoning. - Krystof Hoder; Andrei Voronkov (CADE, 2011)

μZ- An Efficient Engine for Fixed Points with Constraints. - Krystof Hoder; Nikolaj S. Bjørner; Leonardo Mendonça de Moura (CAV, 2011)

Case Studies on Invariant Generation Using a Saturation Theorem Prover. - Krystof Hoder; Laura Kovács; Andrei Voronkov (MICAI (1), 2011)

Invariant Generation in Vampire. - Krystof Hoder; Laura Kovács; Andrei Voronkov (TACAS, 2011)

Vinter: A Vampire-Based Tool for Interpolation. - Krystof Hoder; Andreas Holzer; Laura Kovács; Andrei Voronkov (APLAS, 2012)

Preprocessing techniques for first-order clausification. - Krystof Hoder; Zurab Khasidashvili; Konstantin Korovin; Andrei Voronkov (FMCAD, 2012)

Playing in the grey area of proofs. - Krystof Hoder; Laura Kovács; Andrei Voronkov (POPL, 2012)

Generalized Property Directed Reachability. - Krystof Hoder; Nikolaj S. Bjørner (SAT, 2012)

Practical aspects of automated first-order reasoning. - Krystof Hoder (2012)

The 481 Ways to Split a Clause and Deal with Propositional Variables. - Krystof Hoder; Andrei Voronkov (CADE, 2013)

Selecting the Selection. - Krystof Hoder; Giles Reger; Martin Suda 001; Andrei Voronkov (IJCAR, 2016)