报告题目：构建程序的正确性证明 (The logics to establish the correctness of programs)

报告人：曹钦翔 （普林斯顿大学计算机系）

报告时间地点：12月16日(周二）下午15:10-18:00，北京大学三教108室

报告摘要:不正确的计算机程序(Programs)可能导致一系列的不良后果，例如计算机系统安全漏洞、软件行为异常等等。
然而，大量现有的软件是由上百万行的计算机程序写成的，在这样的数量级下，程序员很难保证其开发的程序不存在一些微小的疏忽。最近十年来，学术界开发了大量工具用以避免错误的程序。而为程序配上机器可检验的正确性证明(Program with proof)就是诸多进路之一。这次报告将主要介绍构建程序正确性证明的逻辑基础。

报告大纲:
1. 如何描述程序的正确性: 霍尔逻辑(Hoare Logic)
2. 基本的数据存储模型
3. 链表结构与Separation Logic
4. 函数与Step Indexing