一個案例說明高層屬性形式化驗證

1.驗證軟件功能介紹： Beosin-VaaS的業務邏輯驗證軟件, 是一款用來檢測智能合約上層業務邏輯漏洞的軟件。 基於合約的白皮書, 軟件利用形式化方法, 首先對單個函數進行屬性的描述, 在對單個函數進行屬性的驗證並通過後, 基於這些已驗證屬性, 抽取出高層的狀態屬性, 進而對上層屬性進行自動推理和驗證, 若屬性不滿足, 則會返回一條反例路徑。 2.案例介紹（界面：合約。） 我們可以以下面這個案

>>阅读原文<<