Software Model Checking for Verifying Distributed Algorithms

We have developed a new approach to producing high-assurance distributed software. Our approach, a form of verifying compilation, consists of verification using a new domain-specific language for writing distributed algorithms and code generation.