A buffer overflow benchmark for software model checkers. - Kelvin Ku; Thomas E. Hart; Marsha Chechik; David Lie (ASE, 2007)

Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates. - Thomas E. Hart; Kelvin Ku; Arie Gurfinkel; Marsha Chechik; David Lie (ASE, 2008)

PtYasm: Software Model Checking with Proof Templates. - Thomas E. Hart; Kelvin Ku; Arie Gurfinkel; Marsha Chechik; David Lie (ASE, 2008)