Homepage of Kryštof Hoder
I am a PhD graduate from the School of Computer Science of the University of Manchester, my supervisor was Andrei Voronkov. My resume can be downloaded here.
My work on the Vampire theorem prover
Unfortunatelly, I no longer work on Vampire.
The Vampire theorem prover should be available for download at vprover.org. Become fan of Vampire.
If you are struggling with Vampire, and unofficial readme can be found here.
Work done
 160,000 lines of code (14 March 2012)
 Atom equivalence detection using Simultaneous SAT sweeping
 Congruence closure algorithm
 SMTLIB1.2 parser
 Several preprocessing rules based on quantified AIGs
 Predicate definition inlining
 Proof localization
 Interpolant minimization using an external SMT solver
 Tabulation based proof search algorithm
 InstGen calculus
 Global subsumption resolution (using our prooftracking SAT solver)
 Unitresulting resolution
 Preprocessing rules for predicate definitions and preserving/restoring EPR in their presence
 API for formula manipulation and clausification
 Let...in and ifthenelse constructs
 Participation on the CASCJ5 competition
The new version of Vampire (0.6) has won the FOF, CNF and LTB divisions.  Limited multiprocessing support implemented for reasoning with large theories
 100,000 lines of code reached! (29 June 2010)
 Evaluation of interpreted symbols
 Efficient work with large theories
 Forward subsumption and demodulation indexing based on code trees
 Various methods of clause splitting
 Colouring of signature symbols with retrieval of interpolants and output of consequences of symbol eliminating inferences
 Participation on the CASC22 competition
In combination with an old version of Vampire it has won the FOF division, and (using the SInE axiom selection) also the LTB division.  Use of binary decision diagrams and an incremental SAT solver to handle propositional predicates
 Discount, Otter and LRS saturation algorithm implementation
 Substitution tree index implementation
My other work
As part of the CASC travel prize, I have visited in February 2012 the Theorem Proving Group at TU Munich and gave four talks: Automated Theorem Proving and Vampire, Sine Axiom Selection, Interpolant Minimization with Proof Transformations and Fixed Points and the μZ Engine (parts of the slides are reused from my coauthors' presentations)
Coorganiser of the Firstorder theorem proving and Vampire tutorial, held as part of the CADE 2011 conference on August 1, 2011 in Wroclaw, Poland. My slides on Vampire usage are here, examples used in the slides here.
Efficient Datalog engine extended with means to handle infinite domains. Implemented during internship in Microsoft Research as part of the Z3 SMT solver. (slides)
Unification index benchmarking — a framework for comparing unification indexes based on COMPIT.
SInE — axiom selection system, winner of the CASCJ4 (and in some sense also CASC22 and CASCJ5) LTB division.
Publications [DBLP]

Generalized property directed reachability, K. Hoder, N. Bjorner
Accepted to SAT 2012 
Playing in the Grey Area of Proofs, K. Hoder, L. Kovacs, A. Voronkov
POPL 2012 
Case Studies on Invariant Generation Using a Saturation Theorem Prover, K. Hoder, L. Kovacs, A. Voronkov
MICAI 2011 
Sine Qua Non for Large Theory Reasoning, K. Hoder, A. Voronkov
CADE 2011 (slides) 
μZ — An Efficient Engine for Fixedpoints with Constraints, K. Hoder, N. Bjorner, L. de Moura
CAV 2011 (my slides from Dagstuhl presentation) 
Invariant Generation in Vampire, K. Hoder, L. Kovacs, A. Voronkov
TACAS 2011 
Evaluation of Automated Theorem Proving on the Mizar Mathematical Library, J. Urban, K. Hoder, A. Voronkov
ICMS 2010 
Symbol Elimination and Interpolation in Vampire, K. Hoder, L. Kovacs, A. Voronkov
IJCAR 2010 
Comparing Unification Algorithms in FirstOrder Theorem Proving, K. Hoder, A. Voronkov
KI 2009
Contact
Google Profile