分离逻辑（separation logic），理学-计算机科学技术-计算机软件-软件基础理论-程序验证，一种支持指针程序验证的程序逻辑。是对霍尔逻辑的扩充。分离逻辑在2000年前后由J.C.雷诺兹（John C.Reynolds）等人提出，其目标是能够更加简洁、直观地描述指针数据结构（如单链表、二叉树等）并验证对这些数据结构进行操作的带指针的程序。分离逻辑对霍尔逻辑的扩充主要体现在状态断言的扩充和霍尔三元组的推理规则的修改和扩充。其状态断言在一阶逻辑断言基础上引入下列描述内存的断言：①，表示内存为空，即无可用内存；②，表示内存中有且仅有一个内存单元，其地址为，存储的值为；③，称为分离合取（separating conjunction），表示内存可以分为地址不相交的两块，它们分别满足断言和；④，称为分离蕴涵（separating implication），表示如果在现有内存的基础上补充一块与之不相交的、满足的内存，那么补充后的内存满足。分离逻辑的断言能够简洁的表达指针之间是否具有别名关系，这也是指针程序验证中面临的重要问题。