owned this note
owned this note
Published
Linked with GitHub
# Formal methods 共筆區
## 簡介
這裡有篇不錯的簡介文
介紹整個領域
[基于逻辑的形式化验证方法:进展及应用](http://www.xml-data.org/BJDXXBZRB/html/2016-2-363.htm#outline_anchor_6)
[计算的极限（十二）：不会出错的程序](https://fwjmath.wordpress.com/2016/02/17/the-limit-of-computation-12/)
[计算机科学名人堂：Jean-Raymond Abrial](http://blog.sciencenet.cn/blog-1225851-847436.html)
[形式化方法 ｜形式化方法对软件开发的挑战：历史与发展](http://www.sohu.com/a/147590425_610499)
## 語法區
目前是學習Isabelle/HOL的語法
[Isabelle/HOL語法探索區](https://hackmd.io/OwNghgLATArBYFoYA4AMATBEDMKEE5t0AjLAY2QFMBGSsaqYs9IA?both)
## proof K
目前研究這[library](https://isabelle.in.tum.de/dist/library/HOL/HOL-Hoare/index.html)中
現在要不要教證明 , 我還在猶豫
因為我發現有人有寫好 , 似乎可以code自動抽象化的library
需要教的理由是:
萬一遇到library無法處理的code
還是需要人來
-----------------------
Isabelle/HOL
比較特別一點
如果是要寫證明腳本
反而文件不去看比較好
先去看library
[Isar](https://isabelle.in.tum.de/dist/library/HOL/HOL-Isar_Examples/index.html)
文件當作字典用
------------
給自己的簡單驗證題
```
int a = 1;
a = a + 3;
```
證明
```
a=4
```
我試試看用那個library來證
bad import........
又該翻文件了
----------------
把一些跟同學討論的說法貼上來
```
它可能
還需要用到能量守恆之類守恆律的概念
記憶體管理模組
就是一個要使用這種不變量的概念
分出去的記憶體位址和還沒分配的記憶體位址 必須是整個硬體可能的記憶體位址
這有個前提
可能記憶體位址 不隨著時間增加
如果是一個自動化可以新增硬體的系統
驗證更黑暗
```
----------
開始找Hoare Logic相關的資料
[Hoare Logic wiki](https://en.wikipedia.org/wiki/Hoare_logic)
[一份投影片](https://www.cs.cmu.edu/~aldrich/courses/413/slides/24-hoare.pdf)
[2011 Hoare Logic 教材](http://www.cl.cam.ac.uk/~mjcg/Teaching/2011/Hoare/Lectures/L3.Oct12.a4.pdf)
[另一份教材](http://flolac.iis.sinica.edu.tw/flolac12/lib/exe/flolac12.pdf)
這份目前讀起來比上面的清楚
[Isabelle/HOL Hoare library 文件](http://isabelle.in.tum.de/dist/library/HOL/HOL-Hoare/document.pdf)
[另一份提到點歷史的教學文件](https://users-cs.au.dk/amoeller/talks/hoare.pdf)
[關於分離邏輯(很有用)](https://wenku.baidu.com/view/dfec028171fe910ef12df88d.html)
[Hoare Logic](https://zh.wikipedia.org/wiki/%E9%9C%8D%E5%B0%94%E9%80%BB%E8%BE%91)
[程序验证技术——霍尔逻辑](http://blog.lucode.net/programming-language/PV-HoareLogic.html)
[一個Coq 面向大眾的電子書](https://github.com/MarisaKirisame/SFCT/blob/master/Preface.v)
[fb使用Hoare Logic做code驗證的例子](http://www.jianshu.com/p/c289cfae49ce)
[Hoare Logic投影片](http://www.cse.yorku.ca/~lesperan/Roma09PhDcourse/slides/lecture4/Part2-HoareLogic09.pdf)
-----------------------------------
接下來還是只能找paper了
我發現我要證的
不能算是一個lemma
應該要算是公理
所以還是得想一個新的
貼個Hoare library中的例子好了
```
lemma "VARS x y z::nat
{y = z & z ≠ 0} z ≠ 0 → x := y div z {x = 1}"
by vcg_simp
```
Output 訊息
```
theorem {y = z ∧ z ≠ 0}
z ≠ 0 → x := y div z
{x = 1}
```
看起來是Hoare Logic三元組的形式沒錯
因為example都沒有code(連結死了)
所以還在猜
唯一有的文件
就是Hoare library中的Readme
-----------------------
```
目前整理
Hoare Logic用於一般的code
分離邏輯用於資料結構
HOL-Hoare_Parallel
是Hoare的推廣 用在平行與並行
```
-----------------------
看了library的定義
才發現是抽象化的符號表示有問題
```
datatype 'a com =
Basic "'a ⇒ 'a"
| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
```
我們需要Basic的
對 , 要表示成若p則q
所以
```
int a=1;
a=a+3
```
就是表示為
```
lemma aux:"VARS a::nat
{a=1}a=1→a:=a+3{a=4}"
by vcg_simp
```
看下面的output
```
theorem aux: {a = 1}
a = 1 → a := a + 3
{a = 4}
```
Hoare Logic三元組出現了
----------------------
看library
都用VARS來證
那Valid不知拿來做啥的
一個成功的IF例子
C code:
```
if(a<7)
{
a = 9;
}
```
Isabelle/HOL code
```
lemma aux_1:"VARS t::nat
{a=t} IF a<7 THEN (a<7→a:=9) ELSE (a≥7→a:=a) FI{(a=9)∨(a=t)}"
by vcg_simp
```
下方視窗Output訊息
```
theorem aux_1: {?a = t}
IF ?a < 7 THEN ?a < 7 → SKIP ELSE 7 ≤ ?a → SKIP FI
{?a = 9 ∨ ?a = t}
```
------------------------------------
把上面兩段code合併
```
int a = 1;
a = a + 3;
if(a < 7)
{
a = 9 ;
}
```
來嘗試證a=9
---------------------
拉拉拉 , 終於有進度了
Isabelle/HOL code
```
lemma aux_2:"VARS a::nat
{a = 1}
(a=1→a:=a+3);
IF a < 7 THEN a:=9 ELSE a:=a FI
{a = 9}"
by vcg_simp
```
Output 訊息
```
theorem aux_2: {a = 1}
a = 1 → a := a + 3; IF a < 7 THEN a := 9 ELSE SKIP FI
{a = 9}
```
-----------------------------------
突破
下一個要攻克的 : 循環不變式
------------------------------------
目前猜測的循環不變式
是一個若p則q的形式
p->q
```
有一個曾經找過數的集合
有一個還沒找過數的集合
兩個聯集是整個要比的array內數的集合
然後定義一個推理規則 , 從沒找過數的集合 , 取出一個數去聯集曾經找過數的集合
還需要另一個推理規則 , 把還沒找過數的集合去掉剛剛取出數的集合
這樣若p則q , 就是數學歸納法中的
第i項 , 推i+1項
```
哈哈
array的抽象化type定義成功
兩個推理規則也弄好了
```
datatype order_fin_array = Empty_Array | sub_array nat order_fin_array
```
```
primrec get_nat::"order_fin_array ⇒ nat"where
"get_nat Empty_Array = 0"|
"get_nat (sub_array n p) = n"
```
```
primrec get_sub_array::"order_fin_array ⇒ order_fin_array"where
"get_sub_array Empty_Array = Empty_Array"|
"get_sub_array (sub_array n p) = p"
```
----------------------
又到了給自己寫簡單證明題的時間了
考慮下列簡單的while loop
```
int a[2];
a[0] = 1;
a[1] = 2;
int i = 0;
int max = 0;
while(i < 2)
{
max = max + a[i];
i = i + 1;
}
```
證max=3
唉唉........
該不會要去學ML才能好好的定義函數吧......
----------------------------------------
喔喔喔喔
```
lemma test_while:"VARS a i max
{True}
i:=0;max:=0;
a[0]:=1;
a[1]:=2;
WHILE i<2
INV{i≤length a}
DO max:=max+(a!i);i:=i+1 OD
{max=3}"
apply vcg_simp
```
看output訊息
```
proof (prove)
goal (3 subgoals):
1. ⋀a. (a ≠ [] ⟶ Suc 0 < length a) ∧ a ≠ []
2. ⋀a i. i ≤ length a ∧ i < 2 ⟹ Suc i ≤ length a
3. ⋀a i max. i ≤ length a ∧ ¬ i < 2 ⟹ max = 3
```
看來就是欠缺找正確的循環不變式(邏輯敘述)
----------------------------------------
目前proof script改成這樣
```
lemma test_while:"VARS a i max
{(length a) = 2}
i:=0;
max:=0;
a[0]:=1;
a[1]:=2;
WHILE i<(length a)
INV{ i≥0 ∧ i≤length a ⟶ (if i=0 then max=0 else max=(∑j=0..(i-1). a!j) ) }
DO max:=max+(a!i);i:=i+1 OD
{max=3}"
apply vcg_simp
```
output訊息
```
proof (prove)
goal (2 subgoals):
1. ⋀a i max.
(i ≤ length a ⟶
(if i = 0 then max = 0 else max = sum (op ! a) {0..i - 1})) ∧
i < length a ⟹
max + a ! i = sum (op ! a) {0..i}
2. ⋀a i max.
(i ≤ length a ⟶
(if i = 0 then max = 0 else max = sum (op ! a) {0..i - 1})) ∧
¬ i < length a ⟹
max = 3
```
-------------------------------------------
看library 跟array有關的例子
```
lemma zero_search: "VARS A i
{True}
i := 0;
WHILE i < length A & A!i ~= key
INV {!j. j<i --> A!j ~= key}
DO i := i+1 OD
{(i < length A --> A!i = key) &
(i = length A --> (!j. j < length A --> A!j ~= key))}"
apply vcg_simp
apply(blast elim!: less_SucE)
done
```
第一個apply的output訊息
```
proof (prove)
goal (1 subgoal):
1. ⋀A i t.
(∀j<i. A ! j ≠ key) ∧
i ≤ length A ∧ t = Suc i ∧ i < length A ∧ A ! i ≠ key ⟹
∀j<Suc i. A ! j ≠ key
```
第二個apply的output訊息
```
proof (prove)
goal:
No subgoals!
```
這個proof script對應code的意義是
找出某個在array中元素的index
example array相關有個有趣的lemma
```
lemma lem: "m - Suc 0 < n ==> m < Suc n"
by arith
```
--------------------------------------
貼一下Hoare library Readme的符號使用
```
VARS x y ... {P} prog {Q}
where prog is a program in the above language, P is the precondition, Q the postcondition, and x y ... is the list of all program variables in prog. The latter list must be nonempty and it must include all variables that occur on the left-hand side of an assignment in prog. Example:
VARS x {x = a} x := x+1 {x = a+1}
The (normal) variable a is merely used to record the initial value of x and is not a program variable. Pre/post conditions can be arbitrary HOL formulae mentioning both program variables and normal variables.
The implementation hides reasoning in Hoare logic completely and provides a method vcg for transforming a goal in Hoare logic into an equivalent list of verification conditions in HOL:
apply vcg
If you want to simplify the resulting verification conditions at the same time:
apply vcg_simp
which, given the example goal above, solves it completely. For further examples see Examples.
IMPORTANT: This is a logic of partial correctness. You can only prove that your program does the right thing if it terminates, but not that it terminates.
```
全部Basic在學過Hoare Logic的基礎上
--------------------------------------
```
proof (prove)
goal (2 subgoals):
1. ⋀a i max.
(i ≤ length a ⟶
(if i = 0 then max = 0 else max = sum (op ! a) {0..i - 1})) ∧
i < length a ⟹
max + a ! i = sum (op ! a) {0..i}
2. ⋀a i max.
(i ≤ length a ⟶
(if i = 0 then max = 0 else max = sum (op ! a) {0..i - 1})) ∧
¬ i < length a ⟹
max = 3
```
看來while只能乖乖寫腳本了 , 無法一行文......
------------------------------------------
所以array相關的還是可以的
```
lemma test:"VARS a
{length a=2}
a[0]:=1;
a[1]:=3
{a!0=1∧a!1=3}"
by vcg_simp
```
output 訊息
```
theorem
test: {length a = 2}
0 < length a → a := a[0 := 1]; 1 < length a → a := a[1 := 3]
{a ! 0 = 1 ∧ a ! 1 = 3}
```
把上面後置的邏輯敘述改成
```
(a!0+a!1) = 4
```
來看看會有什麼結果
應該是還是正確的Hoare 三元組
```
lemma test:"VARS a
{length a=2}
a[0]:=1;
a[1]:=3
{(a!0+a!1) = 4}"
by vcg_simp
```
output訊息
```
theorem
test: {length a = 2}
0 < length a → a := a[0 := 1]; 1 < length a → a := a[1 := 3]
{a ! 0 + a ! 1 = 4}
```
果然是正確的
當然 , 後置的邏輯敘述
是要跟自己想證明code的正確性有關
這邊只是舉例
-------------------------------
乖乖先蹲後跳
搞懂apply與對應tag的使用
還有Isar.....
while相關的 , 看example幾乎都無法一行文(也有一行文的)
需要整理些Main內建的lemma
----------------------------------------
[偏向程式證明的教學課程](http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php)
想先把這課程的pdf整理
來有系統的學習apply與Isar
要不然循環不變式真的證不了
-------------------------------------------
恩
關於example
一個gcd算法的驗證蠻有趣的
在想那方法能不能用在array上
-------------------------------------
放棄array的相加
直接弄跟科普類似的例子
```
lemma "VARS i max list
{length list = 2}
i:=0;
max:=0;
list[0]:=1;
list[1]:=3;
WHILE i < (length list)
INV{∀j. j≤i⟶(((list!j)≤max)∨max=0)}
DO (IF list!i>max THEN max:=list!i ELSE max:=max FI;i:=i+1) OD
{∀j. j≤(length list)⟶(list!j)≤max}"
```
output訊息
```
proof (prove)
goal (2 subgoals):
1. ⋀i max list.
(∀j≤i. list ! j ≤ max ∨ max = 0) ∧ i < length list ⟹
(max < list ! i ⟶
(∀j≤Suc i. list ! j ≤ list ! i ∨ list ! i = 0)) ∧
(¬ max < list ! i ⟶ (∀j≤Suc i. list ! j ≤ max ∨ max = 0))
2. ⋀i max list.
(∀j≤i. list ! j ≤ max ∨ max = 0) ∧ ¬ i < length list ⟹
∀j≤length list. list ! j ≤ max
```
看來還是先把2011的教材弄份2016可以跑的
--------------------------------------
寫例子的時候
弄懂parser tree的錯誤訊息了
如下例子:
```
primrec append::"'a list ⇒ 'a list ⇒ 'a list"(infixr "@" 65)where
"[] @ y = y"|
"(x # D) @ y = x # (D @ y)"
```
@是不能在""內使用的
x @ y 是換一個符號表示
x @ y = append x y
看錯誤訊息
```
Ambiguous input⌂ produces 2 parse trees:
("\<^const>HOL.Trueprop"
("\<^const>HOL.eq"
("\<^fixed>append" ("\<^const>List.list.Nil") ("_position" y))
("_position" y)))
("\<^const>HOL.Trueprop"
("\<^const>HOL.eq"
("\<^const>List.append" ("\<^const>List.list.Nil") ("_position" y))
("_position" y)))
Ambiguous input
2 terms are type correct:
(([] @ y) = y)
(([] @ y) = y)
Failed to parse prop
```
看上面的
```
HOL.Trueprop
HOL.eq
```
Trueprop代表True的前提(邏輯敘述)
eq是代表方程式的意思
就是xxx=oooo
這種東西
所以可以看到它跟柯里-霍華德同構實做檢查算法需要用到的資料結構
有很密切的關係
(個人以為語法不是很完整 , 所以才需要再寫ML
這在Hoare Logic的library有ML的code)
---------------------------------------
一個簡單的實驗
[連結](https://hackmd.io/BwNgrATA7AhjCmBaYx4GZEBYAMxvPgGMJEoAjQ7AE2IDMKIyg===)中的一個lemma
```
lemma append_Nil2[simp]: "append xl [] = xl"
apply (induct xl)
apply (simp add:append_def)
apply (simp )
done
```
當移動到
```
apply (induct xl)
```
output訊息
```
proof (prove)
goal (2 subgoals):
1. pdf_example.append [] [] = []
2. ⋀a xl.
pdf_example.append xl [] = xl ⟹
pdf_example.append (a # xl) [] = a # xl
```
看的出來是使用數學歸納法阿
apply固定作用在第一個subgoal
所以接下來
```
apply (simp add:append_def)
```
output訊息
```
proof (prove)
goal (1 subgoal):
1. ⋀a xl.
pdf_example.append xl [] = xl ⟹
pdf_example.append (a # xl) [] = a # xl
```
這就是要證第i個 , 下一個會成立
移動到
```
apply (simp )
```
output訊息
```
proof (prove)
goal:
No subgoals!
```
都證完拉
所以就done停止吧
output訊息
```
theorem local.append_Nil2: pdf_example.append ?xl [] = ?xl
```
--------------------------------------
補充一篇簡介文 , 對新接觸的同學比較容易理解
另外修正了科普解說文
抽象化模型與code的不一致性
----------------------------------------
有點進展拉
```
proof (prove)
goal (3 subgoals):
1. ⋀i max list.
(max = 0 ∨ (∀j<i. list ! j ≤ max)) ∧ i < length list ⟹
max < list ! i ⟹ ∀j<Suc i. list ! j ≤ list ! i
2. ⋀i max list.
(max = 0 ∨ (∀j<i. list ! j ≤ max)) ∧ i < length list ⟹
¬ max < list ! i ⟶ max = 0 ∨ (∀j<Suc i. list ! j ≤ max)
3. ⋀i max list.
(max = 0 ∨ (∀j<i. list ! j ≤ max)) ∧ ¬ i < length list ⟹
∀j≤length list. list ! j ≤ max
```
把subgoal拆成這樣了
對應的code
```
`lemma "VARS i max list
{length list = 2}
i:=0;
max:=0;
list[0]:=1;
list[1]:=3;
WHILE i < (length list)
INV{(max=0)∨(∀(j::nat). j<i⟶list!j≤max)}
DO (IF (list!i)>max THEN max:=list!i ELSE SKIP FI;i:=i+1) OD
{∀j. j≤(length list)⟶(list!j)≤max}"
apply vcg_simp
apply (rule conjI)
apply (rule impI)
apply (rule disjI2)
```
在想利用set , 這個操作可以把list變成set
這樣會不會比較好做
----------------------------------------
改了循環不變式
現在的code變成
```
lemma "VARS i max (list::nat list)
{length list = 2}
i:=0;
max:=0;
list[0]:=1;
list[1]:=3;
WHILE i < 2
INV{if i = 0 then max = 0 else (∀j<i. list!j ≤ max) }
DO (IF (list!i)>max THEN max:=list!i ELSE SKIP FI;i:=i+1) OD
{∀j. j≤(length list)⟶(list!j)≤max}"
```
使用apply vcg_simp
要證的subgoal變成
```
proof (prove)
goal (2 subgoals):
1. ⋀i max list.
(if i = 0 then max = 0 else ∀j<i. list ! j ≤ max) ∧ i < 2 ⟹
(max < list ! i ⟶ (∀j<Suc i. list ! j ≤ list ! i)) ∧
(¬ max < list ! i ⟶ (∀j<Suc i. list ! j ≤ max))
2. ⋀i max list.
(if i = 0 then max = 0 else ∀j<i. list ! j ≤ max) ∧ ¬ i < 2 ⟹
∀j≤length list. list ! j ≤ max
```
看起來變簡單了
改的原因在於 , 循環不變式必須while command前是True
while後還是True
之前的個人以為有問題
----------------------------------------
發現之前建錯了
不過終於有一個驗證過的有while command的程式
```
lemma "VARS i max (list::nat list)
{length list =2}
i:=0;
max:=0;
list[0]:=1;
list[1]:=3;
WHILE i < 2
INV{(if i=0 then max=0 else (∀j<i . list!j≤max))}
DO (IF (list!i)>max THEN max:=list!i ELSE SKIP FI;i:=i+1) OD
{∀j<i. list!j≤max}"
apply vcg_simp
apply (rule conjI)
apply (rule impI)
apply (rule )
apply (rule impI)
apply (erule less_SucE)
apply auto
apply (erule less_SucE)
apply auto
done
```
看output訊息
```
theorem
{length list = 2}
i := 0;
max := 0;
0 < length list → list := list[0 := 1];
1 < length list → list := list[1 := 3];
WHILE i < 2 INV {if i = 0 then max = 0 else ∀j<i. list ! j ≤ max}
DO IF max < list ! i THEN max := list ! i ELSE SKIP FI; i := i + 1
OD
{∀j<i. list ! j ≤ max}
```
不過這只是證明了max可以大於等於array內的數
還沒證明它是array內最大的數
就差個max是array內的數
---------------------------------------
改了imports的theory
command就正常了
看來不能直接imports Hoare
------------------------------------------
新增新文章的區域
預計把澳洲新南威爾斯大學所開設的課程
做讀書筆記與共筆
以及MIT今年的課程
[新南威爾斯大學 Formal method課程](http://cs4161.web.cse.unsw.edu.au/lect.html)
[MIT課程](https://frap.csail.mit.edu/main)
----------------------------------------
lemma "(a::nat)#((0::int)#[]) = [a , 0]"
output訊息:
```
Type unification failed: Clash of types "int" and "nat"
Type error in application: incompatible operand type
Operator: op # a :: nat list ⇒ nat list
Operand: [0] :: int list
```
看來跟OCaml一樣
type參數都要是相同
所以之前寫的文章
任意type的講法是錯的
---------------------------------
第一部入門影片release拉
[形式化驗證入門](http://hackfoldr.org/formal/)
## 舊文區
Coscup演講以前的文章
有些內容是錯誤的
### 形式化驗證文章
[淺談Curry–Howard isomorphism(柯里-霍華德同構)](https://hackmd.io/KwIwHApgDAZsYFoBMICcATBAWKBDAbAmPgMwRECMJJWSYSA7FjKkA===?both)
[CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels 想法](https://hackmd.io/KYJgDALAhgJgrCAtAYzgDgoiB2SioBsBMiIAnAEZkBmy1cAzFAxEA===?both)
[binary_search簡易解說](https://hackmd.io/EwDgRgrAjAJgDAUwLQGMQ2QFjQNiQTjBmCWDgGYB2AM3IjjBAUyA?both)
[什麼是證明](https://hackmd.io/EYDgDA7AJgZgbAJgLQQCwGYRNWBEkCcAxhHEsHEQKxgCG6MUEMIQA===?both)
[lean code 如何閱讀](https://hackmd.io/IYBmEYFMHZwVgLQCMBMwDMCAsXoA4E8A2NbAEyRD2khADMiog===?both)
[一題證明題的思路](https://hackmd.io/KYEwHAZgDATFDsBaAnGGBmRAWdBGGiARjLroiCPOmPAGxYCGEthQA===?both)
[一個lean old_library的例子說明-兼談關於rust:binary search的abstract specification](https://hackmd.io/KYMwxgjAnALADAJgLQFYDsUBGSYggEyQEMUwokwyEJSA2EFKEIA=?both)
[一個討論](https://www.facebook.com/microjserv/posts/10155165405417389)
[形式化驗證的公理系統](https://hackmd.io/KwIwzMCmCMYCwFoDsAzAhgTgXAxjpCGAHDokcdGkQCY4pwjVA===?both)
#### 牛刀小試
[科普演算法做形式化驗證的提示](https://hackmd.io/JwYwLCCsCMkAwFpKQEbQWATAdgIYJQDMwATBEEsSEktaaEkIA===?both)
[科普演算法 形式化驗證解答與說明](https://hackmd.io/IwVgJgxgzARgTADgLQgGxwkgLFsUkJwgCcSYADOQOzFUCmEAZnQIZxA=)
[2011 形式化驗證基礎課程例子整理](https://hackmd.io/BwNgrATA7AhjCmBaYx4GZEBYAMxvPgGMJEoAjQ7AE2IDMKIyg===)
#### 談談數學
[什麼是代數](https://hackmd.io/MwIwrA7AZlCMwFpYQGwBMEBY0GMCmCIKAhgEwIohrA6kAMdAHDhJkA==)
[定理造算法:以梯度下降法為例](https:// "title")
## 新文章
[用4523659424929個符號定義1](http://sa.ylib.com/MagArticle.aspx?Unit=columns&id=3635)
[高文院士JDD演講全文：AI發展浮沉60年，這一波高潮我們還能走多遠？（附PPT）](http://bangqu.com/624463.html)
[My first experience with Formal Methods](http://zipcpu.com/blog/2017/10/19/formal-intro.html)
###### tags: `formal verification`
Google Drive
Gist
Clipboard
Sign in with Wallet
