2013-2014学年

1：程序验证简介

  • 程序验证-内容-讲义.ppt
  • 软件系统行为与程序正确性-稿件.pdf

    -- 预备知识

  • 程序验证-相关基础-讲义.ppt
  • 预备知识-习题.pdf

    2：程序与系统模型

  • Krikpe结构基本概念-讲义.rar (2013-9-24)
  • 自动机、时间自动机、Petri网基本概念-讲义.rar (2013-10-10)

  • 程序与系统模型-稿件.pdf
  • 程序与系统模型-讲义.pdf
  • 程序与系统模型-例子2a.ppt
  • 程序与系统模型-例子2b.ppt
  • 程序与系统模型-例子2c.ppt
  • 程序与系统模型-例子2d.ppt

    3：程序逻辑

  • 时序逻辑基本概念-讲义.rar (2013-10-23)

  • 程序逻辑-稿件.pdf
  • 程序逻辑-讲义.pdf
  • 程序逻辑-例子.ppt
  • 程序逻辑-例子LTL.ppt
  • 程序逻辑-例子CTL.ppt

    4：程序的推理验证

  • 程序的推理验证-稿件.pdf (2011-11-25)

  • 程序的推理验证-讲义.pdf (2011-11-25)

  • 程序的推理验证-例子.pdf (2013-11-11)

  • 程序的推理验证-证明.pdf (2011-11-01)

  • 程序的推理验证辅助工具veri2.tar.gz 例子

    5：程序的模型检测

  • 程序的模型检测-稿件.pdf

  • 程序的模型检测-讲义.pdf

  • 程序的模型检测-例子.pdf

  • 程序的模型检测-例子BDD与限界模型.ppt

  • CTL模型检测总结.ppt

  • LTL模型检测总结.ppt

  • 模型检测工具VERDS网页 工具说明与例子
  • VERDS例子: mutual exclusion
  • VERDS例子: integer square root
  • 通讯协议模型检测-例子.ppt

    6：课程总结

  • 程序验证-内容.ppt

    部分习题解答

  • l1n09exe.pdf
  • l2n14exe.pdf
  • l3n09exe.pdf
  • 与[](p->(aUb))等价的自动机
  • l4n09exe.pdf
  • l5n09exe.pdf

    2012-2013学年

    1：程序验证简介

  • 程序验证-简介-讲义.ppt
  • 程序验证-内容-讲义.ppt
  • 程序验证-简介-稿件.pdf

    -- 预备知识

  • 程序验证-相关基础-讲义.ppt
  • 预备知识-稿件.pdf

  • 预备知识-习题.pdf
  • 模型检测-习题.doc

    2：程序与系统模型

  • 程序与系统模型-稿件.pdf

  • 程序与系统模型-讲义.pdf

  • 程序与系统模型-例子2a.ppt

  • 程序与系统模型-例子2b.ppt

  • 程序与系统模型-例子2c.ppt

  • 程序与系统模型-例子2d.ppt

  • 互斥算法模型检测-例子.ppt

  • 通讯协议模型检测-例子.ppt

    3：程序逻辑

  • 程序逻辑-稿件.pdf

  • 程序逻辑-讲义.pdf

  • 程序逻辑-例子.ppt

  • 程序逻辑-例子LTL.ppt

  • 程序逻辑-例子CTL.ppt

    4：程序的推理验证

  • 程序的推理验证-稿件.pdf (2011-11-25)

  • 程序的推理验证-讲义.pdf (2011-11-25)

  • 程序的推理验证-例子.pdf (2011-11-01)

  • 程序的推理验证-证明.pdf (2011-11-01)

  • 程序的推理验证辅助工具veri2.tar.gz 例子

    5：程序的模型检测

  • 程序的模型检测-稿件.pdf

  • 程序的模型检测-讲义.pdf

  • 程序的模型检测-例子.pdf

  • 程序的模型检测-例子BDD与限界模型.ppt

  • 模型检测工具VERDS网页 工具说明与例子

    2011-2012学年

    1：程序验证简介

  • 程序验证-简介-讲义.ppt
  • 程序验证-简介-稿件.pdf (2011-11-25)

    -- 预备知识

  • 程序验证-相关基础-讲义.ppt .pdf

  • 预备知识-稿件.pdf

  • 预备知识-习题.pdf

    2：程序与系统模型

  • 程序与系统模型-稿件.pdf (2011-11-01)

  • 程序与系统模型-讲义.pdf (2011-11-01)

  • 程序与系统模型-例子2a.ppt .pdf (2011-9-23)

  • 程序与系统模型-例子2b.ppt .pdf (2011-9-16)

  • 程序与系统模型-例子2c.ppt .pdf (2011-10-8)

  • 程序与系统模型-例子2d.ppt .pdf (2011-10-8)

    3：程序逻辑

  • 程序逻辑-稿件.pdf (2011-11-25)

  • 程序逻辑-讲义.pdf (2011-11-25)

  • 程序逻辑-例子.ppt (2011-11-01)

  • 程序逻辑-例子LTL.ppt (2011-10-11)

  • 程序逻辑-例子CTL.ppt (2011-10-11)

    4：程序的推理验证

  • 程序的推理验证-稿件.pdf (2011-11-25)

  • 程序的推理验证-讲义.pdf (2011-11-25)

  • 程序的推理验证-例子.pdf (2011-11-01)

  • 程序的推理验证-证明.pdf (2011-11-01)

  • 程序的推理验证辅助工具veri2.tar.gz 例子

    5：程序的模型检测

  • 程序的模型检测-稿件.pdf (2011-12-01)

  • 程序的模型检测-讲义.pdf (2011-12-01)

  • 程序的模型检测-例子.pdf (2011-11-17)

  • 程序的模型检测-例子BDD与限界模型.ppt (2011-12-01)

  • 模型检测工具SPIN网页 例子

  • 模型检测工具SMV网页 例子

  • 模型检测工具VERDS网页 工具说明与例子

    6：课程总结

  • 课程总结-讲稿 (2011-12-01)

    2010-2011学年

    1：程序验证简介(1)

  • 程序验证简介1 - 讲义.ppt/讲稿.pdf

  • 程序验证简介2 - 讲义.ppt

    2：预备知识(5)

  • 预备知识 - 稿件.pdf

    2：程序与系统模型(13+1)

  • 程序与系统模型 - 稿件.pdf

  • 程序与系统模型 - 讲义.pdf (2009-10-21)

  • 程序与系统模型 - 例子gcd.pdf (2009-10-20)

  • 程序与系统模型 - 例子mutex.pdf (2009-10-20)

  • 程序与系统模型 - 例子vend.pdf (2009-10-20)

    3：程序逻辑(10)

  • 程序逻辑 - 稿件.pdf

  • 程序逻辑 - 讲义.pdf (2009-10-29)

  • 程序逻辑 - 例子.pdf (2009-10-29)

    4：程序的推理验证(10)

  • 程序的推理验证 - 稿件.pdf

  • 程序的推理验证 - 讲义.pdf (2009-11-23)

  • 程序的推理验证 - 例子mutex.pdf (2009-11-23)

  • 程序的推理验证 - 例子root.pdf (2009-11-23)

  • 程序的推理验证 - 例子misc.pdf (2009-11-23)

  • 程序的推理验证 - 证明.pdf (2009-12-18)

  • 程序的推理验证辅助工具veri2 .tar.gz 例子

    5：程序的模型检测(3)(0.5/3+1.0/3)

  • 程序的模型检测- 稿件.pdf

  • 程序的模型检测- 讲义.pdf (2010-1-4)

  • 程序的模型检测- 例子.pdf (2010-1-6)

  • 模型检测工具SPIN 网页 例子

  • 模型检测工具SMV 网页 例子

    6：课程总结(1)(0.5/3)

  • 课程总结- 讲稿.ppt