Minat dan Keahlian

Metodologi pengujian konvensional, meskipun efektif dalam aplikasi skala besar, tidak dapat membuktikan bahwa suatu perangkat lunak sepenuhnya bebas dari bug. Domain aplikasi kritis seperti penerbangan, eksplorasi luar angkasa, transportasi, layanan kesehatan, dan keuangan menuntut perangkat lunak yang digunakan dalam bidang ini harus benar-benar sesuai dengan spesifikasi. Kesalahan dalam perangkat lunak pada domain ini dapat menyebabkan kerugian finansial yang sangat besar atau, dalam skenario terburuk, mengakibatkan korban jiwa. Bidang formal verification dan metode formal berfokus pada pengembangan teknik dan alat untuk menjamin tingkat keamanan tertinggi dengan memastikan dan membuktikan bahwa sistem yang mendasarinya tidak memiliki bug. Saya mulai mengeksplorasi bidang ini sekitar dua dekade lalu sebagai bagian dari penelitian magister saya.

Meskipun teknik umum dalam formal verification memberikan dasar untuk eksplorasi state-space dalam suatu sistem, pemahaman tentang semantik bahasa pemrograman, sistem tipe, analisis program, dan kompilator memungkinkan adaptasi beberapa teknik formal verification untuk sistem perangkat lunak. Bahasa pemrograman seperti Rust dan Move berusaha meningkatkan kualitas perangkat lunak dengan mengikuti prinsip "Pencegahan lebih baik daripada pengobatan" melalui sistem tipe yang kuat. Paradigma pemrograman fungsional kini mulai diadopsi dan dipopulerkan dalam berbagai bahasa pemrograman imperatif. Prinsip desain bahasa pemrograman semacam ini sangat membantu dalam penalaran otomatis terhadap perangkat lunak. Saya telah menjadi penulis atau memberikan kontribusi utama pada berbagai alat analisis program, software verification, dan perbaikan otomatis seperti Pinaka, CBugs, AtomicInf, CBMC-Repair, 2LS, LLOV, GPURepair, dan lainnya.

Banyak alat penalaran otomatis bergantung pada representasi program sebagai seperangkat kendala (constraints). Solusi terhadap kendala ini sering kali dapat dipetakan ke bug yang mungkin muncul selama eksekusi. Jika tidak ada solusi yang ditemukan, maka ini menunjukkan tidak adanya bug dalam program. Constraint solvers tercanggih (misalnya, SAT/SMT solvers) mampu menangani jutaan kendala. Constraint programming sebagai bidang penelitian berfokus pada pengembangan teknik untuk menemukan solusi terhadap kumpulan kendala dengan kecepatan ekstrem atau membuktikan bahwa tidak ada solusi yang mungkin. Saya telah menjadi penulis atau memberikan kontribusi utama pada solver seperti OpenWBO, OpenWBO-Inc, Shesha, dan CryptoMiniSAT.

Blockchain dapat dianggap sebagai eksekusi mesin status deterministik. Melakukan "eksekusi" ini secara terdesentralisasi dan toleran terhadap kesalahan memerlukan pemahaman dalam penelitian sistem terdistribusi. Di Supra, kami mengembangkan DORA sebagai protokol kesepakatan oracle terdistribusi yang inovatif untuk merancang blockchain oracle yang cepat, skalabel, transparan, dan tangguh.

Komentar

Di Supra, saya telah terlibat dalam perancangan protokol oracle yang sangat tangguh, cepat, skalabel, dan transparan. Blockchain sebagai bidang penelitian memiliki banyak potensi karena menawarkan berbagai aplikasi nyata yang penting. Kita telah menyaksikan penggunaan blockchain dalam sektor keuangan dan game. Beberapa pemerintah bahkan sudah memanfaatkan blockchain sebagai registri yang tidak dapat diubah untuk menyimpan catatan properti tak bergerak (misalnya, tanah) dan mata uang digital bank sentral.

Potensi blockchain untuk mengurangi litigasi dalam berbagai transaksi bisnis tidak terbatas. Teknologi ini dapat memungkinkan berbagai transaksi bisnis antara pihak-pihak yang tidak saling percaya, sekaligus menegakkan SLA dan ketentuan yang telah disepakati, sehingga mempercepat proses transaksi bisnis. Selain aplikasi-aplikasi ini, diperlukan juga solusi untuk berbagai masalah penelitian yang berkaitan dengan privasi dan jaminan keadilan.

Bimbingan Mentorship

Saurabh Joshi telah membimbing beberapa mahasiswa magister dan PhD dalam penyusunan tesis mereka di IIT Hyderabad. Sebagai anggota fakultas, ia telah mengajar Principles of Programming Languages, Introduction to Programming, Software Development Fundamentals, dan Software Engineering di tingkat sarjana, serta Constraint Programming dan Software Verification di tingkat pascasarjana.