Preliminary Analysis of Isabelle Proof Assistant in Graph Programming Verification with GP2 - Dalam bentuk pengganti sidang - Artikel Jurnal
MARTIN HUTAPEA
Informasi Umum
Kode
23.04.7173
Klasifikasi
620.103 - Applied statics
Jenis
Karya Ilmiah - Skripsi (S1) - Reference
Subjek
Applied Mathematics
Dilihat
197 kali
Informasi Lainnya
Abstraksi
<p>GP2 is a graph transformation rule-based graph programming language that facilitates analysis and verification of programs. Verification of a graph program with GP2 can be done with formal proof in first-order or monadic second-order logic. The process of verifying a graph program tends to be complex if it is done manually. This paper discusses the result of the preliminary analysis of the utilization of Isabelle as a proof assistant to help show the validity of a graph program. This study aims to see how much Isabelle can be used as a proof assistant to verify a graph program in GP2. Experimental results show that complex theory is one of the factors in Isabelle’s failure to prove certain properties. The research results show that Isabelle can verify some properties for graph program verification, but it is limited to certain theories.</p>
<p>Keywords: GP2, graph program, Isabelle, proof assistant</p>
- CII4E4 - TUGAS AKHIR
Koleksi & Sirkulasi
Tersedia 1 dari total 1 Koleksi
Anda harus log in untuk mengakses flippingbook
Pengarang
| Nama | MARTIN HUTAPEA |
| Jenis | Perorangan |
| Penyunting | Gia Septiana Wulandari, Muhammad Arzaki |
| Penerjemah |
Penerbit
| Nama | Universitas Telkom, S1 Informatika |
| Kota | Bandung |
| Tahun | 2023 |
Sirkulasi
| Harga sewa | IDR 0,00 |
| Denda harian | IDR 0,00 |
| Jenis | Non-Sirkulasi |
