As presented by Landon Taylor, Sanghamitra Roy, and Zhen Zhang.
See https://formal-verification-research.github.io for more information
This repository contains the files used as part of our research to formally verify a fault-tolerant livelock-free routing algorithm for a mesh network.
Within each folder, steps to recreate our results are enumerated.
| Directory | Description |
|---|---|
| arbitration | Verifying correctness of the handshake arbitration protocol and the network architecture. See Sections 5 and 6 in our paper. |
| old_ideas | Our non-working model (useful to understand limitations of invariant checking) |
| routing | Correct verification of the routing protocol using C++ simulation. |
| zones | Using scripts to formally verify the zone-based model |