Simplified simulation models for indoor MANET evaluation are not robust. - Horacio Andrés Lagar-Cavilla; Gerard Baron; Thomas E. Hart; Lionel Litty; Eyal de Lara (SECON, 2004)

Making lockless synchronization fast: performance implications of memory reclamation. - Thomas E. Hart; Paul E. McKenney; Angela Demke Brown (IPDPS, 2006)

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

On the Robustness of Simple Indoor MANET Simulation Models. - H. Andrés Lagar-Cavilla; Gerard Baron; Thomas E. Hart; Lionel Litty; Eyal de Lara (Ad Hoc Sens. Wirel. Networks, 2007)

Performance of memory reclamation for lockless synchronization. - Thomas E. Hart; Paul E. McKenney; Angela Demke Brown; Jonathan Walpole (J. Parallel Distributed Comput., 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)

Security Benchmarking using Partial Verification. - Thomas E. Hart; Marsha Chechik; David Lie (HotSec, 2008)

Average-Case "messy" Broadcasting. - Chenkuan Li; Thomas E. Hart; Kevin J. Henry; Ian A. Neufeld (J. Interconnect. Networks, 2008)