随着计算机的普及应用，计算机程序的正确性证明变得越来越重要。演绎验证是一种重要的程序正确性证明方法。它用逻辑公式描述程序性质，用一组公理和规则进行推导，从而能够证明程序满足某些性质。分离逻辑是一种演绎验证方法。本文主要研究分离逻辑对并发程序的描述及验证。　　 为描述并发程序，Zohar Manna及Amir Pnueli定义了一个并发程序描述语言SPL。SPL用发送、接受语句来描述并发进程之间的通讯，这种方法比较直观。为研究并发程序的编译机制，Richard Bornat等人用分离逻辑来描述并发程序的资源管理性质，将整个共享状态看作命名资源的划分集合，在任何时刻，整个状态可以被每个进程划分成分离的部分，而每个分离部分都满足相应的资源不变式，并用条件临界区命令及其相应的推理规则来刻画临界区。　　 为全面理解并发程序的实现机制，本文研究了SPL的描述与验证方法，主要工作有：　　 ●基于分离逻辑给出了SPL的公理语义，包括信道的描述，发送、接收语句的推导规则等。　　 ●给出了SPL的指称语义并利用指称语义证明了上述推导规则的可靠性。　　 ●用上述推理系统描述和验证了某些经典的并发系统：生产者消费者问题，互斥问题、读者写者问题。　　 随着多核时代的到来，人们越来越关心多线程、并发程序设计，对并发程序的研究有重要的现实意义。本文基于分离逻辑给出了一种更直观、应用更广泛的并发程序描述和验证方法。