Benjamin Kiesl-Reiter
Computer ScientistI'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
benjamin.kiesl[at]gmail.com
Software
Awards and Nominations
Publications
Solving String Constraints with Concatenation Using SAT
To appear in: Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design (FMCAD 2024).
Proofs for Incremental SAT With Inprocessing [pdf]
In: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD 2023).
Solving String Constraints Using SAT [pdf | bibtex]
In: Proceedings of the 35th International Conference on Computer Aided Verification (CAV 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
Propositional Proof Skeletons
In: Proceedings of the 29th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023). [pdf | bibtex]
Migrating Solver State [pdf | bibtex]
In: Proceedings of the 25th Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Best Paper Nomination
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.
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).
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).
Simulating Strong Practical Proof Systems with Extended Resolution [pdf | bibtex]
In: Journal of Automated Reasoning.
Truth Assignments as Conditional Autarkies [pdf | bibtex]
In: Proceedings of the 17th Symposium on Automated Technology for Verification and Analysis (ATVA 2019).
QRAT Polynomially Simulates ∀-Exp+Res [pdf | bibtex]
In: Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 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.
Clausal Proofs of Mutilated Chessboards [pdf | bibtex]
In: Proceedings of the 11th NASA Formal Methods Symposium (NFM 2019).
Structural Reasoning Methods for Satisfiability Solving and Beyond [pdf | bibtex]
PhD Thesis.
Strong Extension-Free Proof Systems [pdf | bibtex]
In: Journal of Automated Reasoning.
Local Redundancy in SAT: Generalizations of Blocked Clauses [pdf | bibtex]
In: Logical Methods in Computer Science (LMCS), vol. 14(4:3).
Extended Resolution Simulates DRAT [pdf | bibtex]
In: Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018). Best Paper Award.
PRuning Through Satisfaction [pdf | bibtex]
In: Proceedings of the 13th Haifa Verification Conference (HVC 2017). Best Paper Award.
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).
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).
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.
Short Proofs Without New Variables [pdf | bibtex]
In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26). Best Paper Award.
The Potential of Interference-Based Proof Systems [pdf | bibtex]
In: Proceedings of the 1st ARCADE Workshop (ARCADE 2017).