2017 Coscup Formal verification Demo

這是存放演講Demo資料的地方

使用2016-1版的Isabelle/HOL

建議使用GUI的界面

各個file的意義如下

slide.pdf

演講的投影片

demo.c

被形式驗證的c code

編譯輸出執行檔可以show出結果

Try_.thy

給聽者練習證明的檔案

已經建立好模型

只剩補完要證的邏輯敘述與證明腳本

要證的性質寫在註解

(*

....
....

*)

註解符號

answer.thy

其中一種證明腳本的實作

ref

Formal methods 共筆區

形式化驗證 (Formal Verification)

Taiwan Linux Kernel Hackers

Background reading on Hoare Logic.pdf

演講補充資料