4 posts
Kaniのような境界付きモデル検査器やAlloyのような関係モデルファインダーは、通常のアサーションと制約で性質を検証できる。活性の証明を諦める代わりに、学習曲線は週ではなく時間単位で測られる。
モデル検査器を使うために線形時相論理を学ぶ必要はない。Kani、CBMC、Alloyのようなツールは、通常のアサーションと関係制約で性質を検証できる。活性を証明する能力と引き換えに、学習曲線は週ではなく時間単位で測られ、ほとんどのソフトウェアのバグに対してそれは見合う交換だ。…
Kani のようなモデル検査ツールを使えば、形式的証明の代わりに表明で Rust の性質を検証できる。問題は、ループの境界が小さくないときに何が起きるかだ。
一行の証明も書かずに Rust コードの正しさを証明できる。その仕事をするのがモデル検査器であり、現時点で Rust に最も実用的なものは AWS が開発した Kani だ。通常の Rust の表明を書けばよい。Kani…
Differential testingを使えば、正解を知らなくてもバグを見つけられる。問題は、相関した誤りが合意に見えることだ。盲点を見つける方法は以下の通り。
形式的証明がなくてもdifferential testingを信頼できるが、その前提はどこで破綻するかを正確に理解していることだ。 その弱点はcommon-mode failureと呼ばれる。specificationのすべての実装が同じ誤った仮定をした場合、それらはすべて合意し、test…
N-version programmingは実装が一致することを前提とする。テストがなぜ不十分なのか、SMT solverがいかにして等価性を実際に証明できるのか、そして「十分に良い」と「形式的に検証済み」の境界線をどこに引くべきかを見ていく。
n版システムを構築した。同じクリティカルな関数を3つの独立した実装で用意し、多数決で結果を選ぶvoterを置き、単一障害点を凌駕したという満足感に浸っている。 だが、あなたは関数が等価であることを証明していない。コンパイルが通ることを証明したにすぎない。 n-version…