Verifikasi Formal dan Asisten Pembuktian

Verifikasi formal menetapkan, melalui pembuktian matematis yang diperiksa mesin, bahwa perangkat lunak memenuhi spesifikasinya; asisten pembuktian adalah alat yang membangun dan memeriksa pembuktian tersebut.

Definition

Verifikasi formal adalah pembangunan pembuktian yang ketat dan diperiksa mesin bahwa suatu sistem memenuhi spesifikasi formal, dan asisten pembuktian adalah perangkat lunak yang membantu pengguna mengembangkan pembuktian tersebut dan secara mekanis memeriksa validitasnya.

Scope

Topik ini mencakup verifikasi deduktif dan pembuktian teorema interaktif: asisten pembuktian berdasarkan teori tipe atau logika tingkat tinggi (seperti Coq, Isabelle, Lean, dan Agda), pendekatan LCF untuk pembuktian yang dapat dipercaya, dasar proposisi-sebagai-tipe, otomatisasi pembuktian dan taktik, serta artefak terverifikasi penting termasuk kompiler dan kernel sistem operasi.

Core questions

• Bagaimana kebenaran fungsional penuh dapat dibuktikan dan diperiksa mesin?
• Mengapa asisten pembuktian dapat dipercaya, dan apa dasar komputasi tepercaya?
• Bagaimana korespondensi Curry-Howard menghubungkan pembuktian dan program?
• Apa yang diperlukan untuk memverifikasi sistem nyata seperti kompiler dan kernel?

Key theories

Pendekatan LCF untuk pembuktian yang dapat dipercaya

Edinburgh LCF dari Gordon, Milner, dan Wadsworth memperkenalkan kernel pembuktian tepercaya kecil yang harus dilewati semua teorema, sehingga bahkan otomatisasi yang kompleks pun tidak dapat menghasilkan pembuktian yang tidak valid.

Kompiler terverifikasi (CompCert)

CompCert Leroy adalah kompiler C yang terbukti benar dalam asisten pembuktian, dengan teorema yang diperiksa mesin bahwa kode yang dihasilkan menyempurnakan semantik program sumber.

Kernel sistem operasi terverifikasi (seL4)

Klein dan rekan-rekannya menghasilkan pembuktian kebenaran fungsional yang diperiksa mesin untuk mikrokernel seL4, menunjukkan verifikasi ujung-ke-ujung perangkat lunak sistem tingkat rendah.

Clinical relevance

Verifikasi mekanis memberikan jaminan tertinggi yang tersedia untuk perangkat lunak kritis, menghasilkan kompiler, kernel, dan pustaka kriptografi dengan jaminan yang terbukti daripada kepercayaan berbasis pengujian. Asisten pembuktian juga semakin banyak digunakan untuk memformalkan matematika itu sendiri.

History

Pembuktian teorema interaktif dimulai dengan Edinburgh LCF pada tahun 1970-an, yang metalanguage ML dan kernel tepercaya membentuk sistem-sistem selanjutnya. Asisten berbasis teori tipe seperti Coq dan Agda serta sistem logika tingkat tinggi seperti Isabelle/HOL berkembang selama dekade-dekade berikutnya, berpuncak pada artefak terverifikasi penting: kompiler CompCert (2009) dan kernel seL4 (2009).

Debates

Biaya verifikasi versus jaminan yang diperoleh

Membangun pembuktian yang diperiksa mesin untuk sistem besar membutuhkan upaya yang sangat besar, memicu perdebatan tentang di mana verifikasi penuh dibenarkan versus di mana metode yang lebih ringan sudah cukup, dan seberapa banyak pembuktian dapat diotomatisasi.

Key figures

• Robin Milner
• Michael Gordon
• Xavier Leroy
• Gerwin Klein
• Robert Harper

Seminal works

• gordon1979
• leroy2009
• klein2009
• harper2016

Frequently asked questions

Apa itu asisten pembuktian?

Asisten pembuktian adalah perangkat lunak di mana pengguna membangun pembuktian formal secara interaktif sementara sistem secara mekanis memeriksa setiap langkah, sehingga pembuktian yang telah selesai dapat dipercaya hingga kernel yang kecil dan telah diperiksa dengan cermat.

Bagaimana memverifikasi program berbeda dengan mengujinya?

Pengujian memeriksa perilaku pada input yang dipilih dan hanya dapat mengungkapkan keberadaan bug, sementara verifikasi formal membuktikan kebenaran untuk semua input yang diizinkan oleh spesifikasi, menetapkan tidak adanya kesalahan yang ditentukan.