Manos KapritsosAssistant 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.
- 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
TeachingFall 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 servicePLDI 2022