Manos Kapritsos

Assistant Professor
Computer Science & Engineering
University of Michigan, Ann Arbor
4824 Bob and Betty Beyster building

I am interested in increasing the reliability of Distributed Systems. Building reliable distributed systems means guarding against both hardware and software failures. My research spans fault-tolerant replication and formal verification of systems software.

In my most recent projects, I have demonstrated how formal verification can be applied to complex distributed systems; how to verify high-performance cryptographic code; how to rethink replication protocols in the presence of service interactions; how to automate the verification of distributed protocols; and introduced a new approach for verifying high-performance concurrent code.

In previous work, I have shown that the ACID paradigm is not fundamentally slow, but can be made to perform well if one separates the ACID guarantees from the mechanism that implements them; and I have shown how to rearchitect the 40-year-old idea of State Machine Replication to accommodate multithreaded execution.

These days, I mostly work on making formal verification practical by applying it to complex systems in new and interesting ways and by automating the process of proving the correctness of these systems.


News

  • September 2021: We were awarded an NSF Large grant for our proposal on correctness checkability and performance predictability of systems at scale. This is joint work with the University of Chicago and others
  • August 2021: Jon Howell, Rob Johnson and I will be hosting the Systems Software Verification Summer School 2021. You can find more information at this link
  • February 2021: I was awarded the NSF CAREER award
  • July 2020: Jon Howell, Rob Johnson and I hosted the Systems Software Verification Summer School 2020. You can find the recorded lectures and all the relevant material at this link
  • June 2020: Baris Kasikci and I were awarded an NSF FMitF grant to work on automating the verification of distributed systems
  • May 2020: Our paper Armada: Low-Effort Verification of High-Performance Concurrent Programs was awarded the Distinguished Paper Award at PLDI 2020
  • May 2020: Our paper On the Significance of Consecutive Ballots in Paxos was accepted as a Brief Announcement at PODC 2020
  • March 2020: Our paper Armada: Low-Effort Verification of High-Performance Concurrent Programs was accepted at PLDI 2020
  • March 2020: Baris Kasikci, Wes Weimer and I were awarded a DARPA grant to investigate the automatic generation of assured micropatches
  • July 2019: Our paper I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols was accepted at SOSP 2019
  • July 2019: Our paper Aegean: Replication beyond the client-server model was accepted at SOSP 2019
  • September 2018: I was awarded an NSF grant to rethink fault-tolerant replication beyond the client-server model
  • February 2018: I was awarded the Google Faculty Award for 2017
  • August 2017: Our paper Vale: Verifying High-performance Cryptographic Assembly Code got the Distinguished Paper Award at USENIX Security 2017

Teaching

Fall 2021: EECS591 Distributed Systems
Past

Winter 2021: EECS482 Introduction to Operating Systems
Fall 2020: EECS591 Distributed Systems
Winter 2020: EECS482 Introduction to Operating Systems
Fall 2019: EECS591 Distributed Systems
Winter 2019: EECS482 Introduction to Operating Systems
Fall 2018: EECS591 Distributed Systems
Winter 2018: EECS591 Distributed Systems
Fall 2017: EECS482 Introduction to Operating Systems
Winter 2017: EECS591 Distributed Systems

Reviewing service

PLDI 2022
SOSP 2021
OSDI 2021
EuroSys 2021
OSDI 2020
SYSTOR 2020
ICDCS 2020
ATC 2019
NSDI 2019
OSDI 2018
ICDCS 2018
SOSP 2017
DSN 2017