Papers

Security Benchmarking using Partial Verification
Thomas E. Hart, Marsha Chechik, and David Lie. In Proc. 3rd USENIX Workshop on Hot Topics in Security (HotSec'08), San Jose, California, USA, July 2008. [PDF]

Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates (Short Paper)
Thomas E. Hart, Kelvin Ku, David Lie, Marsha Chechik, and Arie Gurfinkel. In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE'08), L'Aquila, Italy, September 2008. [PDF]
     → Extended version appears as a technical report [PDF]

PtYasm: Software Model Checking with Proof Templates (Tool Paper)
Thomas E. Hart, Kelvin Ku, David Lie, Marsha Chechik, and Arie Gurfinkel. In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE'08), L'Aquila, Italy, September 2008. [PDF] [Tool]

A Buffer Overflow Benchmark for Software Model Checkers (Short Paper)
Kelvin Ku, Thomas E. Hart, Marsha Chechik, and David Lie. In Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE'07), Atlanta, Georgia, USA, November 2007. [PDF] [Suite]

On the Robustness of Simple Indoor MANET Simulation Models
H. Andres Lagar-Cavilla, Gerard Baron, Thomas E. Hart, Lionel Litty and Eyal de Lara. Ad Hoc & Sensor Wireless Networks, Volume 4, Number 4, 2007. [PDF]

Performance of memory reclamation for lockless synchronization
Thomas E. Hart, Paul E. McKenney, Angela Demke Brown and Jonathan Walpole. Journal of Parallel and Distributed Computing, Volume 67, Issue 12, December 2007, Pages 1270-1285. [DOI]

Making Lockless Synchronization Fast: Performance Implications of Memory Reclamation
Thomas E. Hart, Paul E. McKenney, and Angela Demke Brown. In Proceedings of the 2006 International Parallel and Distributed Processing Symposium (IPDPS 2006), Rhodes Island, Greece, April 2006. [PDF] [Slides] [Code]
Awarded Best Paper!

Simplified Simulation Models for Indoor MANET Evaluation are not Robust
Andres Lagar Cavilla, Gerard Baron, Thomas E. Hart, Lionel Litty, and Eyal de Lara. In Proceedings of the First IEEE Communications Society Conference on Sensor and Ad Hoc Communications and Networks (SECON), Santa Clara, California, October 2004. [PDF]

Improved Messy Broadcasting in Hypercubes and Complete Bipartite Graphs
Thomas E. Hart and Hovhannes A. Harutyunyan. In Congressus Numerantium vol. 156, pp. 181-195, 2002. [PDF]

Theses

Comparative Performance of Memory Reclamation Strategies for Lock-free and Concurrently-readable Data Structures
Thomas E. Hart. Masters Thesis, Department of Computer Science, University of Toronto, 2005. [PDF]

Talks

Verifying the Absence of Buffer Overflows: Software Model Checking with Proof Templates
Talk which Marsha Chechik and I gave at the MITACS/MASCOS Joint Workshop on Fusion, Mining and Security for Networks in June 2008. [Slides]