摘　要：计算机并发性程序形式化验证一直是软件安全领域的难题。软件并发性漏洞难以被发现，一旦发生问题，会造成不可估量的安全问题。形式化验证基于严格的数学推导基础，采用语言...