Home

Welcome to the prj2_2020 wiki!

选题四：静态检查与程序验证

第一周进展 10.31

阅读 Prusti 论文到第 7 页，理解 rust 类型系统中的 ownership 和 Capabilitie 的概念，开始了解 PCS 算法。（an algorithm to compute precise summaries of the capabilities held at each program point, which we call place capability sets. ）

下一步计划：

尽快在下周阅读完论文。

10.31 和助教讨论记录

根据今晚讨论的结果，我们换一个题目~下面是一些提供给你们的资料，以让你们明白自己大致是要做什么。建议先花1~3周的时间了解一下，就可以正式开始写代码了hhhhh
1. 读教材 CoC 的 Part I，这是你们需要的背景知识
2. 体验一下 Dafny，这是一个非常成熟的验证语言，你们要做的是一个很小的 Dafny
3. 学习一下 Z3 的用法，这是你们需要调用的后端
4. 看一下 Mike He 的 project，这是你们的 baseline：https://zhuanlan.zhihu.com/p/139855937

在 minidecaf step8 的基础上做形式化验证

VARIABLE a,b,c,d

{{ REQUIRES  TRUE }}
{{ ENSURES   c == 45 }}
BEGIN
	a = 10
	b = 0
	c = 0

	WHILE b < a DO
		{{  INVARIANT  c == b*(b-1)/2 }}
	BEGIN
		c = c + b
		b = b + 1
	END
END