CSE Colloquium: Progressive Automated Formal Verification of Hardware and Software Systems

Zoom Information 

Join from PC, Mac, Linux, iOS or Android: https://psu.zoom.us/j/837238333 

or iPhone one-tap (US Toll): +16468769923,837238333# or +13126266799,837238333# 

or Telephone: 

Dial: 

+1 646 876 9923 (US Toll) 

+1 312 626 6799 (US Toll) 

+1 669 900 6833 (US Toll) 

+1 253 215 8782 (US Toll) 

+1 301 715 8592 (US Toll) 

+1 346 248 7799 (US Toll) 

Meeting ID: 837 238 333 

International numbers available: https://psu.zoom.us/u/adBsnTPXaN 

Abstract: Modern computing systems are increasing in complexity, making it challenging to ensure their correctness. 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 design 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. 

Biography: 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 recognized with two best paper nominations, and three of his papers have been honored 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 honors 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.