| 2005 |
| 10 | TVOC: A Translation Validator for Optimizing Compilers. Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck. CAV 2005, 291-295. Web SearchBibTeXDownload |
| 9 | Validating More Loop Optimizations. Ying Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli. Electr. Notes Theor. Comput. Sci. (141): 69-84 (2005). Web SearchBibTeXDownload |
| 8 | Translation and Run-Time Validation of Loop Transformations. Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, Ying Hu. Formal Methods in System Design (27): 335-360 (2005). Web SearchBibTeXDownload |
| 2004 |
| 7 | Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations. Ying Hu, Clark W. Barrett, Benjamin Goldberg. SEFM 2004, 281-289. Web SearchBibTeXDownload |
| 2002 |
| 6 | VOC: A Translation Validator for Optimizing Compilers. Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg. Electr. Notes Theor. Comput. Sci. (65): 2-18 (2002). Web SearchBibTeXDownload |
| 5 | Translation and Run-Time Validation of Optimized Code. Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg, Ying Hu. Electr. Notes Theor. Comput. Sci. (70): 179-200 (2002). Web SearchBibTeXDownload |
| 1997 |
| 4 | Formal Models of Distributed Memory Management. Cristian Ungureanu, Benjamin Goldberg. ICFP 1997, 280-291. Web SearchBibTeXDownload |
| 3 | A Syntactic Method for Finding Least Fixed Points of Higher-Order Functions over Finite Domains. Tyng-Ruey Chuang, Benjamin Goldberg. J. Funct. Program. (7): 357-394 (1997). Web SearchBibTeXDownload |
| 1993 |
| 2 | Real-Time Deques, Multihead Thring Machines, and Purely Functional Programming. Tyng-Ruey Chuang, Benjamin Goldberg. FPCA 1993, 289-298. Web SearchBibTeX |
| 1992 |
| 1 | A Syntactic Approach to Fixed Point Computation on Finite Domains. Tyng-Ruey Chuang, Benjamin Goldberg. LISP and Functional Programming 1992, 109-118. Web SearchBibTeXDownload |