Progressive Automated Formal Verification of Hardware and Software Systems

Modern computing systems are increasing in complexity, making it challenging to ensure their correctness. Despite this, verification is often conducted late in development using empirical testing. This results in bugs being missed, while those that are discovered are found late in development – when the opportunities for fixing them may be limited.

Automated formal verification can provide strong correctness guarantees based on mathematical proofs, but presents a number of challenges. The models used in such verification may be far removed from real implementations, and they may have trouble scaling to the size of real-world systems. In addition, their correctness guarantees may not cover all possible programs.

In this talk, I will discuss how my PhD research has addressed each of these challenges for the verification of Memory Consistency Model (MCM) properties in parallel systems. MCMs specify the ordering and visibility rules for memory operations in parallel programs, so MCM verification is critical to parallel system correctness. My MCM verification work spans the hardware/software stack, and the tools I have developed are designed to be employed at different points in the design timeline. Together, they provide “Progressive Automated Formal Verification”, or automated formal verification throughout the system development process. My MCM work has discovered bugs in a “proven-correct” compiler mapping for C/C++11 atomics, the draft RISC-V ISA’s memory model, a commercial compiler, a lazy coherence protocol, and an open-source processor.

I will conclude with my plans for future work, which include developing new methodologies and tools for the principled design and verification of emerging heterogeneous parallel hardware, applying progressive verification to distributed and cyber-physical systems, and automating the generation of formal hardware specifications.

Bio: Yatin Manerkar is a final-year PhD candidate in the Princeton Computer Science department, advised by Prof. Margaret Martonosi. He holds a BASc in Computer Engineering from the University of Waterloo and an M.S. in Computer Science and Engineering from the University of Michigan. He also worked full-time at Qualcomm Research for one year. Yatin’s research develops automated formal methodologies and tools for the design and verification of computing systems. His work has been recognised with two best paper nominations, and three of his papers have been honoured for their high potential impact as either Top Picks or Honorable Mentions in IEEE Micro’s annual “Top Picks” issue. Yatin is a recipient of the Wallace Memorial Fellowship, one of Princeton’s highest graduate honours awarded to approximately 25 PhD students annually for a senior year of their doctoral studies. He also received the 2019 Award for Excellence from Princeton’s School of Engineering and Applied Science.

11:30-Noon: Grad Student Round Table with the Candidate, 3725 Beyster