4 posts
Bounded model checker seperti Kani dan relational model finder seperti Alloy memungkinkan Anda memverifikasi properti dengan assertion dan constraint biasa. Anda mengorbankan pembuktian liveness untuk kurva pembelajaran yang diukur dalam jam, bukan minggu.
Anda tidak perlu mempelajari logika temporal linear untuk menggunakan model checker. Alat seperti Kani, CBMC, dan Alloy memungkinkan Anda memverifikasi…
Alat model checking seperti Kani memungkinkan Anda memverifikasi properti Rust dengan assertion alih-alih bukti formal. Masalahnya adalah apa yang terjadi ketika loop Anda tidak memiliki batas kecil.
Anda dapat membuktikan kode Rust benar tanpa menulis satu pun bukti. Alat yang melakukannya disebut model checker, dan untuk Rust yang paling praktis saat ini…
Differential testing memungkinkan Anda menemukan bug tanpa mengetahui jawaban yang benar. Masalahnya adalah kesalahan yang saling berkorelasi terlihat seperti kesepakatan. Begini cara menemukan blind spot-nya.
Anda bisa memercayai differential testing tanpa bukti formal, tetapi hanya jika Anda memahami persis di mana ia gagal. Kelemahannya disebut common-mode…
N-version programming mengasumsikan implementasi Anda sepakat. Kita lihat mengapa tes kurang memadai, bagaimana SMT solver bisa benar-benar membuktikan ekuivalensi, dan di mana menarik garis antara cukup baik dan terverifikasi secara formal.
Anda membangun sistem n-version. Tiga implementasi independen dari fungsi kritis yang sama, sebuah voter yang memilih hasil mayoritas, dan perasaan hangat…