Kani

https://gyazo.com/ed70f2322dac02084771618933353f41

モデル検査機(model checker)

Memory safety (e.g., null pointer dereferences)

User-specified assertions (i.e., assert!(...))

The absence of panics (e.g., unwrap() on None values)

The absence of some types of unexpected behavior (e.g., arithmetic overflows)

確認用

Q. Kani

参考

関連