Testudo: Heavyweight security analysis via statistical sampling. - Joseph L. Greathouse; Ilya Wagner; David A. Ramos; Gautam Bhatnagar; Todd M. Austin; Valeria Bertacco; Seth Pettie (MICRO, 2008)

Practical, Low-Effort Equivalence Verification of Real Code. - David A. Ramos; Dawson R. Engler (CAV, 2011)

Under-Constrained Symbolic Execution: Correctness Checking for Real Code. - David A. Ramos; Dawson R. Engler (USENIX Security Symposium, 2015)

Under-constrained symbolic execution : correctness checking for real code. - David A. Ramos (2015)