[静的コード解析の会#6](https://metasepi.connpass.com/event/67805/) で発表した資料です。
前回の発表(https://speakerdeck.com/eldesh/verifast-termination-checking-introduction-a) に続いて、
VeriFastによるC(およびJava)言語の停止性検査について説明しています。
停止性検査を行う背景、基本となる数学的な方針、VeriFastによる検査のアイディア、パターン毎の証明テクニックについて解説しています。
各分類パターンについては具体的なコード(片)に沿って解説しています。
参照:
Modular termination verification
Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper. At ECOOP 2015.