Abstract: 

Modern computing systems underpin critical infrastructure, cloud services, and AI-driven applications — yet answering the timeless question, _“Is my system correct?”_ remains extraordinarily difficult at scale. As hardware and software complexity skyrocket, verification faces a fundamental bottleneck: fully automated techniques collapse under state explosion, while interactive theorem proving demands prohibitive human effort. Verification works — but it does not scale with the systems we build. In this talk, I argue that scalable formal verification lies between these extremes. The key is structured proof decomposition that blends lightweight domain insight with principled automation. Rather than reasoning monolithically about entire systems, we exploit system structure to decompose end-to-end properties into tractable subproblems while preserving strong correctness guarantees. I will present H-Houdini, a scalable verification framework that enables unbounded verification of end-to-end properties on large, real-world hardware designs. Using HHoudini, we verify the Safe Instruction Set Property (SISP) — a foundational microarchitectural security guarantee — on complex out-of-order (OoO) processors such as the RISCV BOOM, the largest most complex open-source OoO processor. These results represent the first scalable verification of such end-to-end security properties on designs of this scale, achieving up to 2800× speedups over prior state-of-the-art approaches, while commercial property checkers fail to complete. This allows us, for the first time, to automatically verify a set of instructions as safe on a microarchitecture enabling provable sound hardware-software defenses against hardware side-channel attacks.

Bio: 

Sushant Dinesh is a postdoctoral researcher in Computer Science at UC Berkeley. His 
research bridges the gap between formal guarantees and system-scale complexity by 
developing scalable verification algorithms for hardware–software systems. He has achieved the first scalable verification of end-to-end security properties on large out-oforder processor designs, with work appearing in PLDI, IEEE S&P, and ASPLOS (Best Paper Award). His long-term goal is to make verification ubiquitous and invisible in practice, providing principled correctness guarantees for the systems that power modern computing