RT DW A1 Yao, Jianan. T1 Automated Verification of Safety and Liveness Properties for Distributed Protocols