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

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 co-authors' presentations)

Co-organiser of the First-order 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 CASC-J4 (and in some sense also CASC-22 and CASC-J5) LTB division.

Publications  [DBLP]




Google Profile