VLDB 2026 Research / reviewers in the wild / expert
Krystof Hoder
dblp:54/7401
· DBLP profile ↗
8ranked-venue papers
8as first author
0since 2021 · last 2013
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 5 · 5 first-authorTheory of computation · 5 · 5 first-authorArtificial intelligence and machine learning · 3 · 3 first-author
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Theoretical computer science
2 papers |
Automated reasoning and model checking · 76% Mathematical optimization · 24% | |
| Software engineering, system software, and programming languages
1 paper |
Program verification · 81% Program analysis · 19% |
Topics — the 7 heaviest of 7, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program verification
interpolation |
0.1 | 1 | 2012 | Playing in the grey area of proofs · POPL 2012 |
Automated reasoning and model checking › model checking
bounded model checking |
0.1 | 1 | 2012 | Playing in the grey area of proofs · POPL 2012 |
Automated reasoning and model checking
constraint solving |
0.1 | 1 | 2011 | μZ- An Efficient Engine for Fixed Points with Constraints · CAV 2011 |
Mathematical optimization
fixed point computation |
0.1 | 1 | 2011 | μZ- An Efficient Engine for Fixed Points with Constraints · CAV 2011 |
Automated reasoning and model checking
model checking |
0.1 | 1 | 2011 | μZ- An Efficient Engine for Fixed Points with Constraints · CAV 2011 |
Program verification
invariant generation |
0.0 | 1 | 2012 | Playing in the grey area of proofs · POPL 2012 |
Program analysis
static analysis |
0.0 | 1 | 2012 | Playing in the grey area of proofs · POPL 2012 |
Methods — techniques the papers use, named apart from their topics
local proofs · 0.3interpolation · 0.3fixed-point computation · 0.1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2013 | The 481 Ways to Split a Clause and Deal with Propositional Variables
Krystof Hoder, Andrei Voronkov |
CADE | 1 |
| 2012 | Vinter: A Vampire-Based Tool for Interpolation
Krystof Hoder, Andreas Holzer, Laura Kovács, Andrei Voronkov |
APLAS | 1 |
| 2012 | Preprocessing techniques for first-order clausification
Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov |
FMCAD | 1 |
| 2012 | Playing in the grey area of proofsabstractInterpolation is an important technique in verification and static analysis of programs. In particular, interpolants extracted from proofs of various properties are used in invariant generation and bounded model checking. A number of recent papers studies interpolation in various theories and also extraction of smaller interpolants from proofs. In particular, there are several algorithms for extracting of interpolants from so-called local proofs. The main contribution of this paper is a technique of minimising interpolants based on transformations of what we call the "grey area" of local proofs. Another contribution is a technique of transforming, under certain common conditions, arbitrary proofs into local ones. Krystof Hoder, Laura Kovács, Andrei Voronkov |
POPL | 1 |
| 2012 | Generalized Property Directed Reachability
Krystof Hoder, Nikolaj S. Bjørner |
SAT | 1 |
| 2011 | Sine Qua Non for Large Theory Reasoning
Krystof Hoder, Andrei Voronkov |
CADE | 1 |
| 2011 | μZ- An Efficient Engine for Fixed Points with Constraints
Krystof Hoder, Nikolaj S. Bjørner, Leonardo de Moura 0001 |
CAV | 1 |
| 2011 | Invariant Generation in Vampire
Krystof Hoder, Laura Kovács, Andrei Voronkov |
TACAS | 1 |