我們可以使用Z3 SMT求解器進行SW測試

Question

我們可以使用Z3來做軟件的功能驗證。例如，如果我有一個代碼可以說自動售貨機控制器，我們可以使用Z3功能測試它，如果是的話，多少深度，如果沒有爲什麼？

Answer 1

使用SMT解算器進行驗證既「常規完成」，也是學術界和工業界目前研究的主題。尼古拉正在謙虛：我建議先閱讀他的優秀和高度易用的CACM article，其中還包含許多有用的進一步參考資料。