Abstrak Nama: Anggha Satya Nugraha Program studi: Magister Ilmu Komputer Judul: Verifikasi Program Perkalian Matriks Persegi Menggunakan Logika Hoare Karya tulis ini memberikan pembuktian formal dari program perkalian dua matriks persegi sebarang ukuran yang memakai algoritm naive dan juga algoritma Strassen. Untuk membuktikan kebenaran kedua program tersebut, penulis menggunakan sistem pembuktian yang kukuh yaitu sistem pembuktian Hoare. Pertama, kedua algoritma itu dijelaskan secara umum. Kemudian penulis mengeksplorasi logika Hoare yang menjadi dasar sistem pembuktian yang digunakan. Bagian utama dari karya tulis ini adalah pembuktian formal kebenaran sebagian kedua program perkalian matriks tersebut menggunakan sistem pembuktian Hoare. Lebih lanjut, penulis juga mencoba memformalisasikan teori matriks elementer dan logika Hoare dalam HOL theorem prover agar bukti kedua program tersebut dapat dimekanisasi dalam interactive theorem prover. Kata kunci: algoritma