Verification of Faulty Message Passing Systems with Continuous State Space in PVS

We present a library of PVS meta-theories that verifies a class of distributed systems in which agent communication is through message-passing. The theoretic work consists of iterative schemes for solving systems of linear equations, such as message-passing extensions of the Gauss and Gauss-Seidel methods. We briefly review that work and discuss the challenges in formally verifying it.