Manos Kapritsos

Associate 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; introduced a new approach for verifying high-performance concurrent code; and demonstrated how one can reason formally about the performance of a distributed system.

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 (and performance) of these systems.

If you are looking for my verification course material, complete with lecture recordings, slides and Dafny exercises, you can find it here

News

  • April 2023: Our paper Performal: Formal Verification of Latency Properties for Distributed Systems was accepted at PLDI 2023
  • May 2022: Our paper Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems was accepted at USENIX ATC 2022
  • Feb 2022: I was awarded the Jon R. and Beverly S. Holt Award for Excellence in Teaching
  • November 2021: Our paper Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility was accepted at TOPLAS 2021
  • 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 hosted the Systems Software Verification Summer School 2021. The Summer School recordings are no longer available, but you can find a newer version of that material in the page for my new verification course
  • 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. The Summer School recordings are no longer available, but you can find a newer version of that material in the page for my new verification course
  • 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

Winter 2023: EECS482 Introduction to Operating Systems
Past

Fall 2022: Formal Verification of Systems Software
Winter 2022: EECS482 Introduction to Operating Systems
Fall 2021: EECS591 Distributed Systems
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

OSDI 2024
SOSP 2023
HotOS 2023
OSDI 2022
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