www.wklieber.com Open in urlscan Pro
208.94.118.193  Public Scan

Form analysis
0 forms found in the DOM

Text Content

 

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
   William Klieber, Ruben Martins, Ryan Steele, Matt Churilla, Mike McCall,
   David Svoboda.
   In Workshop on Automated Program Repair 2021.
 * Detecting leaks of sensitive data due to stale reads
   Will Snavely, William Klieber, Ryan Steele, David Svoboda, Andrew Kotov.
   In SecDev 2018.
 * Practical Precise Taint-flow Static Analysis for Android App Sets
   William Klieber, Lori Flynn, Will Snavely, Michael Zheng.
   In International Conference on Availability, Reliability and Security (ARES)
   2018.
 * Automated Code Repair Based on Inferred Specifications
   [preprint] [slides: pptx]
   William Klieber, Will Snavely.
   In SecDev 2016.
 * Non-CNF QBF Solving with QCIR
   [preprint]
   Charles Jordan, Will Klieber, and Martina Seidl.
   In Beyond NP 2016.
 * Android Taint Flow Analysis for App Sets
   [preprint] [abstract] [tool souce code] [slides: pptx | pdf ] [DBLP BibTeX]
   William Klieber, Lori Flynn, Amar Bhosale, Limin Jia, Lujo Bauer.
   In SOAP 2014.
 * Solving QBF with Free Variables
   [preprint] [QBF'13 slides] [DBLP BibTeX Record]
   William Klieber, Mikoláš Janota, Joao Marques-Silva, and Edmund M. Clarke.
   In CP 2013.
 * Solving QBF with Counterexample Guided Refinement.
   [preprint] [SAT'12 slides] [alternate slides] [DBLP BibTeX Record]
   Mikoláš Janota, William Klieber, Joao Marques-Silva, and Edmund M. Clarke.
   In SAT 2012.
 * A Non-Prenex, Non-Clausal QBF Solver with Game-State Learning
   [preprint] [Slides] [DBLP BibTeX Record]
   William Klieber, Samir Sapra, Sicun Gao, and Edmund Clarke.
   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:
 * 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)






 

[ 15817 ]