Pada bidang ilmu komputer, pemrograman digunakan oleh peserta didik sebagai media
untuk mengimplementasikan pengetahuan teoritis ke dalam bentuk program. Untuk
memfasilitasi penilaian pada kelas dengan jumlah peserta didik yang banyak,
digunakan sistem penilaian otomatis atau automatic grading. Pendekatan yang populer
digunakan dalam membangun sistem penilaian otomatis saat ini adalah black-box
testing. Penilaian dilakukan dengan menuliskan kumpulan uji kasus untuk
mengeksekusi program peserta didik. Namun, untuk menuliskan kumpulan kasus uji
yang komplit, dalam hal ini mencakup sebanyak mungkin edge cases atau corner
cases, merupakan hal yang sulit untuk dilakukan. Oleh karena itu, perlu dilakukan
eksplorasi pendekatan selain black-box testing pada sistem penilaian otomatis, seperti
white-box testing. Secara teori, dengan memperhatikan isi kode kita dapat mengulas
semua jalur eksekusi yang mungkin, menghasilkan sistem penilaian yang lebih
lengkap.
Pada tugas akhir ini dilakukan penelitian dalam penggunaan analisis semantik sebagai
solusi untuk menentukan kebenaran implementasi program peserta didik. Pada sistem
di tugas akhir ini akan dilakukan perekaman jalur eksekusi implementasi program
referensi dan implementasi program peserta didik, pendeteksian path deviation, dan
pendeteksian path equivalence untuk membandingkan semantik kedua implementasi.
Sistem dibangun dengan memanfaatkan metode concolic execution untuk eksplorasi
dan SMT solver untuk menyelesaikan formula.
Pengujian sistem menunjukkan bahwa penilaian dapat dilakukan dengan melakukan
perbandingan semantik implementasi program referensi dan peserta didik. Berdasarkan
perbandingan dengan pendekatan pembangkitan uji kasus secara acak, ditemukan
kasus–kasus dimana sistem pada tugas akhir dapat memberikan penilaian yang lebih
lengkap.