*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
Tess Malone, Communications Officer
Summary Sentence: Progressive Automated Formal Verification of Hardware and Software Systems
Full Summary: No summary paragraph submitted.
Yatin ManerkarTITLE: Progressive Automated Formal Verification of Hardware and Software Systems
ABSTRACT:
The ubiquity of computing today means that the ramifications of computing bugs are higher than ever. 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 methods can provide strong correctness guarantees based on mathematical proofs, but they present 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 Ph.D. 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. Progressive verification catches bugs earlier than traditional flows, while also amortizing verification overhead over the entire development timeline.
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 Ph.D. candidate in the Princeton computer science department, advised by Professor 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 led to the discovery of bugs in a lazy coherence protocol, a "proven-correct" compiler mapping for C/C++11 atomics, a commercial compiler, and an open-source processor. He has also contributed to the development of the RISC-V ISA's memory model by finding deficiencies in its draft specification. Yatin's research 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.
