|
Will Klieber
(pronounced “KLEE′ ber”)
wklieber
|
|
|
I work in the Secure Coding group at CERT/SEI. Prior to that, I was a Ph.D. student in the Computer Science Dept at Carnegie Mellon
University until I graduated in May 2014. My advisor was
Prof. Edmund Clarke.
My primary research interests include automated software verification and
related technologies, such as SAT/QBF solvers.
|
Recent papers:
- Automated Code Repair to Ensure Spatial Memory Safety
In Workshop on Automated Program Repair 2021. - Detecting leaks of sensitive data due to stale reads
In SecDev 2018. - Practical Precise Taint-flow Static Analysis for Android App Sets
In International Conference on Availability, Reliability and Security (ARES) 2018. - Automated Code Repair Based on Inferred Specifications
[preprint] [slides: pptx]
In SecDev 2016. - Non-CNF QBF Solving with QCIR
[preprint]
In Beyond NP 2016. - Android Taint Flow Analysis for App Sets
[preprint] [abstract] [tool souce code] [slides: pptx | pdf ] [DBLP BibTeX]
In SOAP 2014. - Solving QBF with Free Variables
[preprint] [QBF'13 slides] [DBLP BibTeX Record]
In CP 2013. - Solving QBF with Counterexample Guided Refinement.
[preprint] [SAT'12 slides] [alternate slides] [DBLP BibTeX Record]
In SAT 2012. - A Non-Prenex, Non-Clausal QBF Solver with Game-State Learning
[preprint] [Slides] [DBLP BibTeX Record]
In SAT 2010, LNCS 6175.
Conferences/Workshops:
- Program Committee member, IJCAI 2013.
- Program Committee member, Pragmatics of SAT Workshop 2012.
Teaching:
- TA for 15-453: Formal Languages, Automata, and Computation (Spring 2009).
- TA for 15-212: Principles of Programming (Fall 2010).
Miscellaneous:
- A tweak to IRV to make it a Condorcet method
- GhostQ QBF Solver
- Thesis (PDF): Verification of Software and Hardware using Quantified Boolean Formulas (QBF) | (thesis abstract: HTML)
- QCIR-to-QDIMACS converter
- SAT Solver Slides (PDF)
- Random password generator (based on xkcd 936)
- Do cryptocurrencies use encryption?
- Notes for 15-212 (Principles of Programming)
- Pictures from Korea
Links:
- LaTeX: Using multi-letter variable names in math mode by default
(Add\input{mathmode-spacing.tex}to document preamble) - LaTeX tables: changing line thickness and cell padding (with \arraystretch)
