Profile picture

I am a final-year PhD student in the Princeton Computer Science department, advised by Prof. Margaret Martonosi. My research lies on the boundary between computer architecture and formal methods; specifically on developing automated formal methodologies and tools for the design and verification of computing systems. During my PhD, my research has focused on verification of memory consistency model (MCM) properties in parallel hardware and software. My work has found real-world bugs in C++ compilers, an open-source processor implementation in Verilog, and in the widely-used RISC-V instruction set (ISA).

Before joining Princeton, I completed my BASc in Computer Engineering at the University of Waterloo and a M.S. in Computer Science and Engineering at the University of Michigan. I also worked full-time at Qualcomm Research for one year.

I am a recipient of Princeton's Wallace Memorial Fellowship for the 2018-2019 academic year. The Wallace Memorial Fellowship is a Princeton Honorific Fellowship which provides funding to students displaying the highest scholarly excellence in graduate work during the year. I also received the 2019 Award for Excellence from Princeton's School of Engineering and Applied Sciences (SEAS).

I was selected to attend the 7th Heidelberg Laureate Forum (HLF) in September 2019. The HLF is an annual event where 200 young researchers in computer science and mathematics participate in a weeklong scientific exchange with recipients of the top awards in computing and mathematics (Turing Award, Abel Prize, Fields Medal, ACM Prize in Computing, and the Nevanlinna Prize).

Outside research, I enjoy playing chess, listening to classical music, and reading historical fiction.

My CV can be found here.

I am on the academic job market this year!

Research

Research Statement

We entrust large parts of our daily lives to computer systems, and these systems require thorough verification to ensure their correctness. System vulnerabilities can lead to leakage of confidential information, loss of money, and (in the case of cyber-physical systems) may even threaten one's physical safety and security. Many such bugs have in fact been found in computing systems in recent years, ranging from security vulnerabilities (like Meltdown and Spectre) to network errors to concurrency bugs.

Some important bugs are due to flaws in system design/specification, while others are due to implementations violating the design specification. Since verification is generally focused late in development, bugs tend to get caught late in development as well. Design bugs may necessitate a redesign, wasting the development time spent creating incorrect implementations. Furthermore, many bugs only occur in very specific scenarios, making them hard to find. Current verification processes have proven inadequate for catching these bugs, resulting in the release of flawed hardware and software.

Verification using formal methods provides strong correctness guarantees based on mathematical proofs, and is adept at catching hard-to-find bugs. My work aims to improve the verification of hardware and software using formal methods, without requiring engineers to have formal methods expertise. I propose a philosophy of Progressive Automated Formal Verification, i.e. verification throughout the system development process, from early-stage design through to final implementation. Automating formal verification enables engineering teams to prove strong correctness properties about their designs and implementations by themselves, shifting the verification burden away from the relatively small number of formal methods experts.

In my philosophy, formal models of systems are first created and verified during early-stage design, thus catching design bugs before implementation commences. These models can then evolve to become more detailed as system design progresses. Once the system is implemented, the implementation is formally verified against a proven-correct design model to help ensure implementation correctness. Amortizing verification over the entire design timeline in this manner can reduce verification overhead by finding bugs earlier. The number of steps in a progressive verification flow may vary depending on the type of system being built, but the key idea is to conduct verification throughout the design timeline and link the verification methods at each stage together.

Publications



Refereed Publications

  • Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Aarti Gupta. PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications. The 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), October 2018.
    Nominated for best paper.
    Selected as a IEEE MICRO Top Picks Honorable Mention from the 2018 Computer Architecture Conferences.
    [PDF] [Slides] [Poster] [GitHub]

  • Hongce Zhang, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta, Margaret Martonosi, and Sharad Malik. Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification. The 18th Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2018.
    [PDF]

  • Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. "Full-Stack Memory Model Verification with TriCheck". IEEE Micro, 38 (3) (Top Picks of the 2017 Computer Architecture Conferences), May-June 2018.
    [PDF]

  • Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Michael Pellauer. RTLCheck: Verifying the Memory Consistency of RTL Designs. The 50th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), October 2017.
    Selected as a IEEE MICRO Top Picks Honorable Mention from the 2017 Computer Architecture Conferences.
    [PDF] [Slides] [Poster] [GitHub]

  • Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA. The 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), April 2017.
    Selected as a IEEE MICRO Top Pick from the 2017 Computer Architecture Conferences.
    [PDF]

  • Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. CCICheck: Using µhb Graphs to Verify the Coherence-Consistency Interface. The 48th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), December 2015.
    Nominated for best paper.
    [PDF] [Slides] [Poster] [GitHub]

Non-Refereed Publications

  • Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR abs/1611.01507, November 2016.
    [PDF]

Invited Talks



  • Automated Formal Memory Consistency Verification of Hardware.
    DeepSpec Workshop at PLDI 2019, Phoenix AZ. June 2019.
    [Slides]

  • Automated Full-Stack Memory Model Verification with the Check Suite.
    Imperial College London, UK, July 2018.
    University of Cambridge, UK, July 2018.
    ARM Cambridge, UK, July 2018.
    [Slides]

  • C11 Compiler Mappings: Exploration, Verification, and Counterexamples.
    Dagstuhl Seminar 16471: Concurrency with Weak Memory Models. November 2016.
    [Slides]

Links