5 posts
Cleanroom software engineeringは、デバッグではなくmathematical verificationによって零欠陥のインクリメントを約束した。我々はIBMの実プロジェクトデータを見て、その主張が成り立ったかを確認する。
1980年代のソフトウェア業界平均は、1000行あたり30〜60の欠陥だった。IBMのCleanroomチームは、2万行のコンパイラインクリメントをテストで53の欠陥を発見した状態で出荷した。これはKLOCあたり2.6である。1万行の個別インクリメントの中には、システムテストで欠陥が全く見つからなかったものもあった。…
AutoVerusはLLMエージェントのネットワークを用いてRustコードのVerus正しさ証明を生成し、SMTソルバーのフィードバックによって駆動される生成・修復・ dischargeループにより、90%以上の証明義務を自動化する。
形式的検証で最も難しいのは、検証器そのものではない。証明を書くことだ。 熟練のRustエンジニアにMicrosoft…
Kaniのような境界付きモデル検査器やAlloyのような関係モデルファインダーは、通常のアサーションと制約で性質を検証できる。活性の証明を諦める代わりに、学習曲線は週ではなく時間単位で測られる。
モデル検査器を使うために線形時相論理を学ぶ必要はない。Kani、CBMC、Alloyのようなツールは、通常のアサーションと関係制約で性質を検証できる。活性を証明する能力と引き換えに、学習曲線は週ではなく時間単位で測られ、ほとんどのソフトウェアのバグに対してそれは見合う交換だ。…
Kani のようなモデル検査ツールを使えば、形式的証明の代わりに表明で Rust の性質を検証できる。問題は、ループの境界が小さくないときに何が起きるかだ。
一行の証明も書かずに Rust コードの正しさを証明できる。その仕事をするのがモデル検査器であり、現時点で Rust に最も実用的なものは AWS が開発した Kani だ。通常の Rust の表明を書けばよい。Kani…
N-version programmingは実装が一致することを前提とする。テストがなぜ不十分なのか、SMT solverがいかにして等価性を実際に証明できるのか、そして「十分に良い」と「形式的に検証済み」の境界線をどこに引くべきかを見ていく。
n版システムを構築した。同じクリティカルな関数を3つの独立した実装で用意し、多数決で結果を選ぶvoterを置き、単一障害点を凌駕したという満足感に浸っている。 だが、あなたは関数が等価であることを証明していない。コンパイルが通ることを証明したにすぎない。 n-version…