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 proof-tracking SAT solver)
• Unit-resulting resolution
• Preprocessing rules for predicate definitions and preserving/restoring EPR in their presence
• API for formula manipulation and clausification
• Let...in and if-then-else constructs
• Participation on the CASC-J5 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 CASC-22 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 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]

• 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 Fixed-points 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 First-Order Theorem Proving, K. Hoder, A. Voronkov
  KI 2009

 

Contact

 

 
Google Profile