Adaptive load migration systems for PVM. - Jeremy Casas; Ravi B. Konuru; Steve W. Otto; Robert M. Prouty; Jonathan Walpole (SC, 1994)

MPVM: A Migration Transparent Version of PVM. - Jeremy Casas; Dan L. Clark; Ravi B. Konuru; Steve W. Otto; Robert M. Prouty; Jonathan Walpole (Comput. Syst., 1995)

Logic Verification of Very Large Circuits Using Shark. - Jeremy Casas; Hannah Honghua Yang; Manpreet Khaira; Mandar Joshi; Thomas Tetzlaff; Steve W. Otto; Erik Seligman (VLSI Design, 1999)

A switch level fault simulation environment. - Venkatram Krishnaswamy; Jeremy Casas; Thomas Tetzlaff (DAC, 2000)

Reasoning about GSTE Assertion Graphs. - Alan J. Hu; Jeremy Casas; Jin Yang 006 (CHARME, 2003)

Efficient Generation of Monitor Circuits for GSTE Assertion Graphs. - Alan J. Hu; Jeremy Casas; Jin Yang (ICCAD, 2003)

Accelerator design with decoupled hardware customizations: benefits and challenges: invited. - Debjit Pal; Yi-Hsiang Lai; Shaojie Xiang; Niansong Zhang; Hongzheng Chen; Jeremy Casas; Pasquale Cocchini; Zhenkun Yang; Jin Yang 006; Louis-Noël Pouchet; Zhiru Zhang (DAC, 2022)

Towards A Formally Verified Fully Homomorphic Encryption Compute Engine. - Jeremy Casas; Zhenkun Yang; Wen Wang; Jin Yang 006; Adwait Godbole (DAC, 2023)

Invited: A Scalable Formal Approach for Correctness-Assured Hardware Design. - Jin Yang 006; Jeremy Casas; Zhenkun Yang (DAC, 2023)

An Automated Verification Framework for HalideIR-Based Compiler Transformations. - Yanzhao Wang; Fei Xie 004; Zhenkun Yang; Jeremy Casas; Pasquale Cocchini; Jin Yang 006 (DATE, 2023)

Towards A Correct-by-Construction FHE Model. - Zhenkun Yang; Wen Wang; Jeremy Casas; Pasquale Cocchini; Jin Yang 006 (IACR Cryptol. ePrint Arch., 2023)

Correct-by-Construction Design of Custom Accelerator Microarchitectures. - Jin Yang 006; Zhenkun Yang; Jeremy Casas; Sandip Ray (IEEE Trans. Computers, 2024)

Formal Verification of a Custom Compiler for a Fully Homomorphic Encryption Accelerator. - Zhenkun Yang; Suvadeep Banerjee; Jeremy Casas; Jin Yang 006 (ISQED, 2025)