We present a library of PVS meta-theories that can be used to verify a class of distributed systems in which agent communication is via message-passing. The theoretical work, as outlined in Chandy et al. (Form Aspect Comput 2011, to appear) 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.
- Message passing systems
- Methods for solving systems of linear equations
- PVS theorem-prover
ASJC Scopus subject areas