并发分离逻辑（concurrent separation logic），理学-计算机科学技术-计算机软件-软件基础理论-程序验证，支持对共享内存的并发程序的验证的一种程序逻辑。是对霍尔逻辑和分离逻辑的扩充。并发分离逻辑由两位学者P.奥黑恩[注]（Peter O'Hearn，彼得·奥黑恩）和S.布鲁克斯[注]（Stephen Brookes）于2004年共同提出。并发分离逻辑的基本思想是要求并发任务对共享资源（内存）的访问必须在互斥的临界区中进行。而在临界区之外，并发任务只能访问自己的本地私有资源。要实现这一点，必须有效确保本地私有资源和共享资源的分离，以及不同任务之间的本地私有资源的分离。而分离逻辑中的分离合取恰恰可以用来很方便的描述资源的分离。并发分离逻辑中程序的形式如下：式中表示完成共享资源的初始化工作，第二行语句声明个共享资源，其中每个是资源名，后面跟的变量列表则是资源中使用的变量。每个变量最多只能出现在一个共享资源中。下一行并发语句同时创建个并发任务。当个任务均执行结束的时候，整个程序终止。