金枪鱼之夜:Code is Cheap, Show Me the Proof

时间: 2020-07-04 19:00-21:00 地点: Zoom tunight Coq Formal Verification
资源链接:

众所周知,写出正确的代码从来都不是一件容易的事。虽然不写代码就不会有bug,但是不写代码是不可能的。为了从逻辑上证明某个程序满足某些想要的属性,我们必须采用比测试更加重量级的形式化验证手段。定理证明是一种能验证几乎任何(使用高阶逻辑)属性的证明方法——只要你知道这个定理该怎么证明。这次讲座以知名的证明助理 Coq 为例,从初学者的角度介绍其基本使用。

活动信息:

  • 主讲人:朱俸民
  • 时间:2020/07/04 19:00 UTC +08:00
  • 活动形式:线上会议 + 直播
    • Zoom:685 7505 8025
    • Zoom 直播:https://live.bilibili.com/699121

欢迎一起来玩!

清华大学 TUNA 协会原名清华大学学生网管会,注册名清华大学学生网络与开源软件协会,是由清华大学网络技术和开源软件爱好者、技术宅组成的团体。现阶段向校内外提供开源软件镜像等服务。

The best team on the planet.