实现在Boogie中的并发程序验证工具，核心为Owicki-Gries推理系统，在此基础上引入了： 抽象精化。输入为分层并发程序，底层的实现精化上层的抽象 Mover：右移，左移或者both，指代可以与其他action交换的操作 根据Lipton’s Reduction，形如 Right* a Left* 的语句可以视为原子块 Linear Type 官网有较为详细的介绍