12月16日曹钦翔报告：说明程序正确性的逻辑 (The logics to establish the correctness of programs)
　　不正确的计算机程序可能导致一系列的不良后果，而大量现有的软件是由上百万行的计算机程序写成的，程序员很难保证其开发的程序不存在一些微小的疏忽。为程序配上机器可检验的正确性证明(Program with proof)就是试图避免这一问题的一种方法。这次报告主要介绍用以说明程序正确性的逻辑系统。
　　(1)操作语义(Operational Semantics)。操作语义向最基本的程序语言提供了直观、可靠的语义解释。但在这种语义解释下，对于每一步程序的每一个变量，我们都需要解释。这对于描述程序正确性而言是冗余的。(2)霍尔逻辑(Hoare Logic)。霍尔逻辑的语义对象直接指向程序前后的状态，以此很好地解决了前述的冗余问题。但加入了地址之后，在说明一些程序，诸如交换输入(swapint)程序时，由于需要说明给定的所有地址都是两两不等的，霍尔逻辑也面临表达冗长的问题。(3)分离逻辑(Seperation Logic)。分离逻辑通过定义新的连接词“*”来解决表达上的冗长问题。并且“*”对应的公理满足交换、结合律，因此整个逻辑显得直观而优美。目前，分离逻辑的可靠性已知，而完全性未知。
　　在讨论环节，主讲人就分离逻辑完全性证明的困难之处、程序正确性证明的自动化问题给出了详细的解释，并展示了用以检验程序正确性证明正确与否的程序工具。