"Finding bugs without running or even looking at code" by Jay Parlar

Strange Loop ConferenceYouTube ↗

延伸阅读 1

Parlar 先在 Alloy 中描述设计与希望成立的性质，再检查访问控制等例子里的反例。一个意外实例既可能指出设计漏洞，也可能暴露模型漏写的约束。

视频与逐字稿来源 ↗ · 引文按字幕原文展示，可点时间戳回看片段。

补充字幕原文 2

if the model checker finds any state in which a correctness property fails it'll tell you

we haven't been precise enough in our specification