Abstract

Model checking is an effective method to verify both safety and liveness properties in distributed systems. However, the complexity of model checking grows exponentially with the number of entities which makes it suitable only for small systems. Interactive theorem provers allow for machine-checked proofs. These proofs can include inductive reasoning which allows them to reason about an arbitrarily large number of entities. However, proving safety and liveness properties in these proofs can be difficult. This work explores how combining model checking and inductive proofs can be an effective method for formally verifying complex distributed protocols. This is demonstrated on a part of MyCHIPs, a novel digital currency based on the value of personal credit. It has been selected as a case study because it requires certain properties to hold on a non-trivial distributed algorithm.

Degree

College and Department

Computational, Mathematical, and Physical Sciences; Computer Science

Rights

https://lib.byu.edu/about/copyright/