Compositional Verification
TLA+
Distributed Protocols
Compositional Verification of Distributed Protocols in TLA+
Description
Description and Significance Distributed protocols, e.g. Paxos and Raft, are at the heart of communication for distributed systems. It is very important for these protocols to be correct, yet verifying (proving) their correctness is extremely challenging. In this project, we aim to improve the scalability and performance of tools that are used to verify the correctness of distributed protocols written in the TLA+ formal specification language. In particular, we will be applying compositional techniques to improve the state of the art for model checking (automatically verifying) distributed protocols.
Student Involvement Students will learn about the theory of model checking, including TLA+ and compositional verification. The goal of the project is for the student to implement compositional verification techniques in an existing model checker for the TLA+ language. Students will work with one of two model checkers that our team has been developing: Recomp-Verify and Carini (see the references). Both model checkers are implemented in Java, so students will be expected to write Java code.
References