Benjamin Kiesl

Postdoctoral Researcher at the CISPA Helmholtz Center

I'm a postdoc at the CISPA Helmholtz Center for Information Security in Saarbrücken, Germany, working in the group of Cas Cremers, where we are focusing on the automated verification of security protocols. Before, I did a PhD in computer science under the supervision of Martina Seidl and Hans Tompits at TU Wien.

I have a background in automated reasoning, in particular in SAT solving, but I have also done some work on other formalisms such as first-order logic and quantified Boolean formulas. Together with Marijn Heule and Armin Biere I have developed strong proof systems for propositional logic that lend themselves neatly to automation. We've also come up with a SAT solving paradigm, called Satisfaction-Driven Clause Learning (SDCL), that harnesses the strengths of our proof systems to solve propositional formulas that are (due to inherent theoretical restrictions) too hard for ordinary SAT solvers.

Besides, I know a thing or two about software engineering: I have some professional experience as a software developer, working with C++ (the programming language I'm most familiar with) and Java. I enjoy writing readable code as much as I enjoy writing readable papers and I believe that these two activities have many things in common.

To download my CV, click here.

Contact

Address
Benjamin Kiesl
CISPA – Helmholtz Center for Information Security
Stuhlsatzenhaus 5
66123 Saarbrücken
GERMANY
Email
benjamin.kiesl[at]cispa.saarland

Software

drat2er – A tool that transforms DRAT proofs (as produced by modern SAT solvers) into extended-resolution proofs.

Publications

Benjamin Kiesl and Martina Seidl (2019):
QRAT Polynomially Simulates ∀-Exp+Res [pdf | bibtex]
In: Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019).
Marijn J.H. Heule, Benjamin Kiesl, and Armin Biere (2019):
Encoding Redundancy for Satisfaction-Driven Clause Learning [pdf | bibtex]
In: Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019). Best Paper Nomination.
Marijn J.H. Heule, Benjamin Kiesl, and Armin Biere (2019):
Clausal Proofs of Mutilated Chessboards [pdf | bibtex]
In: Proceedings of the 11th NASA Formal Methods Symposium (NFM 2019).
Benjamin Kiesl (2019):
Structural Reasoning Methods for Satisfiability Solving and Beyond [pdf | bibtex]
PhD Thesis.
Marijn J.H. Heule, Benjamin Kiesl, and Armin Biere (2019):
Strong Extension-Free Proof Systems [pdf | bibtex]
In: Journal of Automated Reasoning.
Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere (2018):
Local Redundancy in SAT: Generalizations of Blocked Clauses [pdf | bibtex]
In: Logical Methods in Computer Science (LMCS), vol. 14(4:3).
Benjamin Kiesl, Adrian Rebola-Pardo, and Marijn J.H. Heule (2018):
Extended Resolution Simulates DRAT [pdf | bibtex]
In: Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018). Best Paper Award.
Marijn J.H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere (2017):
PRuning Through Satisfaction [pdf | bibtex]
In: Proceedings of the 13th Haifa Verification Conference (HVC 2017). Best Paper Award.
Benjamin Kiesl, Marijn J.H. Heule, and Martina Seidl (2017):
A Little Blocked Literal Goes a Long Way [pdf | bibtex]
In: Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT 2017).
Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere (2017):
Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood? [pdf | bibtex]
In: Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI 2017).
Benjamin Kiesl and Martin Suda (2017):
A Unifying Principle for Clause Elimination in First-Order Logic [pdf | bibtex]
In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26). Best Paper Award.
Marijn J.H. Heule, Benjamin Kiesl, and Armin Biere (2017):
Short Proofs Without New Variables [pdf | bibtex]
In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26). Best Paper Award.
Marijn J.H. Heule and Benjamin Kiesl (2017):
The Potential of Interference-Based Proof Systems [pdf | bibtex]
In: Proceedings of the 1st ARCADE Workshop (ARCADE 2017).
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, and Armin Biere (2017):
Blocked Clauses in First-Order Logic [pdf | bibtex]
In: Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21).
Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere (2016):
Super-Blocked Clauses [pdf | bibtex]
In: Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016).