İlgi alanları ve uzmanlık

Geleneksel test metodolojileri, büyük ölçekli uygulamalarda iyi olsa da, bir yazılımın hatasız olduğunu asla kanıtlayamaz. Havacılık, uzay araştırmaları, ulaşım, sağlık ve finans gibi kritik uygulama alanları, bu alanlarda kullanılan yazılımların spesifikasyonlara sıkı sıkıya bağlı kalmasını gerektirir. Bu alanlarda hatalı bir yazılımın yol açtığı hasarlar büyük mali kayıplara ya da en kötü ihtimalle ölümlere neden olabilir. Biçimsel doğrulama ve biçimsel yöntemler alanı, temel sistemin herhangi bir hata içermediğinden emin olmaya ve bunu kanıtlamaya çalışarak en üst düzeyde güvenlik garantileri sağlamak için teknikler ve araçlar geliştirmeye odaklanır. Bu alanı yaklaşık yirmi yıl önce yüksek lisans araştırmamın bir parçası olarak incelemeye başladım.

Biçimsel doğrulamadaki genel teknikler, genel bir sistem için durum uzayı araştırması için temel sağlarken, programlama dili semantiği, tip sistemi, program analizi ve derleyicilerin anlaşılması, yazılım sistemleri için bazı biçimsel doğrulama tekniklerinin masajlanmasına ve benimsenmesine olanak tanır. Rust ve Move gibi programlama dilleri, güçlü tip sistemleri aracılığıyla “Önlemek tedavi etmekten daha iyidir” ilkesini izleyerek yazılım kalitesini artırmaya çalışmaktadır. Fonksiyonel programlama paradigması artık birçok popüler zorunlu programlama dilinde benimsenmekte ve popüler hale gelmektedir. Bu tür programlama dili tasarım ilkeleri, yazılım hakkında otomatik akıl yürütmeye büyük ölçüde yardımcı olmaktadır. Pinaka, CBugs, AtomicInf, CBMC-Repair, 2LS, LLOV, GPURepair, vb. gibi çeşitli program analizi/yazılım doğrulama/otomatik onarım araçları üzerine yazdım/önemli katkılarda bulundum.

Otomatik muhakeme araçlarının çoğu, bir programı bir dizi kısıtlama olarak temsil etmeye dayanır. Bu kısıtlamaların çözümü genellikle yürütme sırasında ortaya çıkabilecek bir hata ile eşleştirilebilir. Kısıtlamalara yönelik herhangi bir çözümün olmaması, herhangi bir hatanın olmadığı anlamına gelir. Son teknoloji kısıt çözücüler (örneğin SAT/SMT çözücüler) milyonlarca kısıtla başa çıkabilmektedir. Bir araştırma alanı olarak kısıt programlama, belirli bir kısıt kümesine aşırı hızlı bir şekilde çözüm bulma veya hiçbir çözümün olmadığını kanıtlama teknikleri geliştirmeye odaklanmaktadır. OpenWBO, OpenWBO-Inc, Shesha ve CryptoMiniSAT gibi çözücüler üzerinde önemli katkılarda bulundum.

Bir blok zinciri, deterministik bir durum makinesinin yürütülmesi olarak yorumlanabilir. Bu “yürütmeyi” merkeziyetsiz ve hataya dayanıklı bir şekilde yapmak, dağıtık sistem araştırmalarından bilgi gerektirir. Supra'da, hızlı, ölçeklenebilir, şeffaf ve esnek bir blockchain oracle'ı tasarlamak için yeni bir dağıtık oracle anlaşma protokolü olarak DORA'yı geliştirdik.

Yorum

Supra'da son derece esnek, hızlı, ölçeklenebilir ve şeffaf bir kehanet protokolünün tasarlanmasında yer aldım. Bir araştırma alanı olarak blok zinciri, birçok önemli gerçek hayat uygulamasına sahip olduğu için sunabileceği çok şey var. Finans ve oyun alanında blockchain kullanımına zaten tanık olduk. Bazı hükümetler, taşınmaz mallar (örneğin arazi) ve merkez bankası dijital para birimleri hakkındaki kayıtları saklamak için değişmez bir kayıt defteri olarak blok zincirlerini halihazırda kullanmaktadır.

Blok zincirinin çeşitli ticari işlemlerde davaları azaltma potansiyeli sınırsızdır. Üzerinde mutabık kalınan SLA'ları ve şartları uygulayarak bu ticari işlemlerin gerçekleşme hızını artırırken, güvenmeyen taraflar arasında çeşitli ticari işlemleri mümkün kılma potansiyeline sahiptir. Bu uygulamaların yanı sıra, gizlilik ve adalet garantileriyle ilgili çeşitli araştırma sorunlarına çözüm bulunması gerekmektedir.

mentorluk

Saurabh Joshi, IIT Hyderabad'da tezleri için birçok yüksek lisans ve doktora öğrencisine danışmanlık yapmıştır. Öğretim üyesi olarak, lisans düzeyinde Programlama Dillerinin İlkeleri, Programlamaya Giriş, Yazılım Geliştirme Temelleri, Yazılım Mühendisliği ve lisansüstü düzeyde Kısıt Programlama, Yazılım Doğrulama dersleri vermiştir.