這是存放演講Demo資料的地方
使用2016-1版的Isabelle/HOL
建議使用GUI的界面
各個file的意義如下
演講的投影片
被形式驗證的c code
編譯輸出執行檔可以show出結果
給聽者練習證明的檔案
已經建立好模型
只剩補完要證的邏輯敘述與證明腳本
要證的性質寫在註解
(*
....
....
*)
註解符號
其中一種證明腳本的實作
Background reading on Hoare Logic.pdf
-
Notifications
You must be signed in to change notification settings - Fork 1
Use to demo
License
KevinKu/Formal-verification-of-simple-C-code
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Use to demo
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published