Benjamin Kiesl-Reiter

Computer Scientist

I'm a Senior Applied Scientist at Amazon Web Services. The main focus of my research is the theory and practice of automated reasoning, aimed at developing techniques that assist us in solving computationally hard problems such as the verification of security protocols, software, and hardware. Together with Niklas Medinger and Cas Cremers I have created and analyzed an extensive formal model of IEEE's WPA2 protocol for wireless security. 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.

I did a PhD in computer science under Martina Seidl and Hans Tompits at TU Wien. After my PhD I did a postdoc at the CISPA Helmholtz Center for Information Security in Saarbrücken, Germany, working in the group of Cas Cremers. I also gained some professional experience as a software engineer at SAP Labs. 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.

Contact

Email
benjamin.kiesl[at]gmail.com

Software

drat2er – A tool that transforms DRAT proofs (as produced by modern SAT solvers) into extended-resolution proofs.
UT Tamarin – If you are using the Tamarin prover to analyze security protocols, this tool will make your life much easier.

Awards and Nominations

2019 Bill McCune PhD Award in Automated Reasoning
Best Paper Award at IJCAR 2018
Two Best Paper Awards at CADE-26
Best Paper Award at HVC 2017
Best Paper Nominations at TACAS 2023 and TACAS 2019
Best Paper Nomination at SAT 2022

Publications

Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, and Dirk Nowotka (2024):
Solving String Constraints with Concatenation Using SAT
To appear in: Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design (FMCAD 2024).
Benjamin Kiesl-Reiter and Michael W. Whalen (2023):
Proofs for Incremental SAT With Inprocessing [pdf]
In: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD 2023).
Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Rupak Majumdar, and Dirk Nowotka (2023):
Solving String Constraints Using SAT [pdf | bibtex]
In: Proceedings of the 35th International Conference on Computer Aided Verification (CAV 2023).
Dawn Michaelson, Dominik Schreiber, Marijn J.H. Heule, Benjamin Kiesl-Reiter, and Michael W. Whalen (2023):
Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers [pdf | bibtex]
In: Proceedings of the 29th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023). Best Paper Nomination
Joseph E. Reeves, Benjamin Kiesl-Reiter, and Marijn J.H. Heule (2023):
Propositional Proof Skeletons
In: Proceedings of the 29th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023). [pdf | bibtex]
Armin Biere, Md Solimul Chowdhury, Marijn J.H. Heule, Benjamin Kiesl, and Michael W. Whalen (2022):
Migrating Solver State [pdf | bibtex]
In: Proceedings of the 25th Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Best Paper Nomination
Armin Biere, Matti Järvisalo, and Benjamin Kiesl (2021):
Preprocessing in SAT Solving [pdf | bibtex]
In: Chapter 9 of Handbook of Satisfiability (2nd ed.), vol. 336, Frontiers in Artificial Intelligence and Applications, pages 391-435, IOS Press 2021.
Cas Cremers, Jaiden Fairoze, Benjamin Kiesl, and Aurora Naska (2020):
Clone Detection in Secure Messaging: Improving Post-Compromise Security in Practice [pdf | bibtex]
In: Proceedings of the 27th ACM Conference on Computer and Communications Security (CCS 2020).
Cas Cremers, Benjamin Kiesl, and Niklas Medinger (2020):
A Formal Analysis of IEEE 802.11’s WPA2: Countering the Kracks Caused by Cracking the Counters [pdf | bibtex]
In: Proceedings of the 29th USENIX Security Symposium (USENIX Security 2020).
Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule, and Armin Biere (2020):
Simulating Strong Practical Proof Systems with Extended Resolution [pdf | bibtex]
In: Journal of Automated Reasoning.
Benjamin Kiesl, Marijn J.H. Heule, and Armin Biere (2019):
Truth Assignments as Conditional Autarkies [pdf | bibtex]
In: Proceedings of the 17th Symposium on Automated Technology for Verification and Analysis (ATVA 2019).
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).