verification

5 posts

cleanroom-correctnesszero-defectsverificationcase-study

Apakah ada yang benar-benar memverifikasi 10.000 baris dengan nol defect? IBM melakukannya, dan metodologinya lebih aneh daripada hasilnya.

Cleanroom software engineering menjanjikan increment zero-defect melalui mathematical verification alih-alih debugging. Kami melihat data proyek IBM yang sebenarnya untuk melihat apakah klaim itu bertahan.

Rata-rata industri perangkat lunak pada tahun 1980-an adalah 30 hingga 60 defect per seribu baris kode. Tim Cleanroom IBM mengirimkan increment compiler 20.000…
model-checkingautoverusrustverification

AutoVerus mengubah 40 jam penulisan proof menjadi 3 panggilan LLM. Triknya adalah tahu kapan harus menyerah.

AutoVerus menggunakan jaringan agen LLM untuk menghasilkan proof kebenaran Verus untuk kode Rust, mengotomatisasi lebih dari 90% proof obligation melalui loop generate-repair-discharge yang didorong oleh feedback SMT solver.

Bagian tersulit dari verifikasi formal tidak pernah ada pada verifier-nya. Ada pada penulisan proof. Beri seorang engineer Rust senior Verus, verifier berbasis…
model-checkingtemporal-logicformal-methodsverification

Anda Dapat Melakukan Model Checking pada Kode Tanpa Mempelajari Temporal Logic

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…
model-checkingrustverificationformal-methods

Anda dapat membuktikan kode Rust benar tanpa menulis satu pun bukti, tapi ruang keadaan adalah tagihannya

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…
n-version-programmingequivalence-testingformal-methodsverification

Tidak Ada Tes yang Bisa Membuktikan Dua Fungsi Ekuivalen. Ini yang Bisa.

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…