Tiến sĩ Saurabh Joshi

Giám đốc Nghiên cứu và Phát triển

Tiến sĩ Khoa học máy tính
Indian Institute of Technology, Kanpur
github-icongoogle-icon
Research Team Member

Tìm hiểu thêm

Tiến sĩ Saurabh Joshi là Nhà nghiên cứu chính tại Supra. Anh đã nhận bằng thạc sĩ từ IIT Bombay trước khi gia nhập nhóm Kỹ sư phần mềm tại IBM India Research. Anh đã nhận bằng tiến sĩ từ IIT Kanpur với chuyên ngành Xác minh phần mềm (Software Verification). Anh là đồng tác giả một bằng sáng chế Hoa Kỳ trong quá trình thực tập nghiên cứu tại Microsoft Research. Anh đã đóng góp quan trọng vào thuật toán và việc triển khai OpenWBO, một trình giải MaxSAT đã giành giải thưởng, trong quá trình sau tiến sĩ tại University of Oxford. Sau một thời gian ngắn làm giảng viên tại IIT Guwahati, anh đã gia nhập IIT Hyderabad cũng với tư cách là giảng viên. Anh đã nhận được hiải thưởng Early Career Research từ DST, Ấn Độ. Anh đã tạo ra Pinaka, một công cụ thực thi biểu tượng nhanh, đứng trong top 3 trong SVCOMP (Cuộc thi xác minh phần mềm) trong một số tiểu danh mục trong vài năm liên tiếp. Anh đã hướng dẫn luận án cho nhiều sinh viên thạc sĩ và tiến sĩ và hoàn thành nhiều dự án nghiên cứu được tài trợ và tư vấn do các công ty tư nhân cũng như các cơ quan chính phủ tài trợ. Anh đã dẫn dắt một nhóm trong nhóm bảo mật sản phẩm tại Qualcomm, chịu trách nhiệm cải thiện bảo mật trong ngăn xếp phần mềm cấp thấp (low-level software stack).

Web3 cung cấp nền tảng yêu cầu giải pháp cho các vấn đề trong nhiều lĩnh vực nghiên cứu khoa học máy tính như hệ thống phân tán, mật mã học, lý thuyết trò chơi, tổ hợp, ngôn ngữ lập trình và xác minh chính thức (formal verification). Bị cuốn hút bởi nhiều vấn đề, anh đã gia nhập Supra. Hiện tại, anh đang làm việc về việc thiết kế oracle blockchain có khả năng mở rộng, nhanh chóng, minh bạch và linh hoạt.

Là một nhà nghiên cứu, anh thích học hỏi và áp dụng các công cụ, kỹ thuật toán học và kỹ thuật khác nhau để giải quyết các vấn đề có tính ứng dụng trong thế giới thực.

Sở thích và chuyên môn

Các phương pháp kiểm tra truyền thống, mặc dù tốt ở khía cạnh ứng dụng quy mô lớn, nhưng không bao giờ chứng minh được phần mềm không có lỗi. Các lĩnh vực ứng dụng quan trọng như hàng không, khám phá không gian, vận tải, chăm sóc sức khỏe và tài chính đòi hỏi phần mềm được sử dụng trong các lĩnh vực này phải tuân thủ chặt chẽ theo thông số kỹ thuật. Thiệt hại do phần mềm lỗi trong các lĩnh vực này có thể gây ra tổn thất tài chính lớn, hoặc trong trường hợp tồi tệ nhất, có thể gây ra nhiều vụ tử vong. Lĩnh vực xác minh chính thức (formal verification) và phương pháp chính thức (formal methods focuses) tập trung vào việc phát triển các kỹ thuật và công cụ để đảm bảo mức độ bảo đảm an toàn cao nhất bằng cách cố gắng đảm bảo và chứng minh rằng hệ thống cơ bản không có bất kỳ lỗi nào. Tôi bắt đầu khám phá lĩnh vực này khoảng hai thập kỷ trước, là một phần của nghiên cứu thạc sĩ của tôi.

Trong khi các kỹ thuật tổng quát trong xác minh chính thức (formal verification) cung cấp cơ sở cho việc khám phá không gian trạng thái cho một hệ thống tổng quát, việc hiểu rõ ngữ nghĩa ngôn ngữ lập trình, kiểu hệ thống, phân tích chương trình và trình biên dịch cho phép một người tùy chỉnh và áp dụng một số kỹ thuật xác minh chính thức cho các hệ thống phần mềm. Các ngôn ngữ lập trình như Rust và Move cố gắng cải thiện chất lượng phần mềm bằng cách tuân theo nguyên tắc "Phòng ngừa tốt hơn chữa trị" thông qua hệ thống mạnh mẽ của họ. Mô hình lập trình chức năng (functional programming) hiện đang được áp dụng và phổ biến trong nhiều ngôn ngữ lập trình mệnh lệnh (programming langauges). Nguyên tắc thiết kế ngôn ngữ lập trình như vậy hỗ trợ rất nhiều trong việc suy luận tự động về phần mềm. Tôi là tác giả/đóng góp chính vào nhiều công cụ phân tích chương trình/xác minh phần mềm/sửa chữa tự động như Pinaka, CBugs, AtomicInf, CBMC-Repair, 2LS, LLOV, GPURepair, v.v.

Nhiều công cụ suy luận tự động dựa vào việc biểu diễn một chương trình dưới dạng một tập hợp các ràng buộc. Giải pháp cho những ràng buộc này thường có thể được ánh xạ thành một lỗi có thể xuất hiện trong quá trình thực thi. Việc không có bất kỳ giải pháp nào cho các ràng buộc này ngụ ý rằng không có bất kỳ lỗi nào. Các trình giải ràng buộc tiên tiến (ví dụ, trình giải SAT/SMT) có khả năng xử lý hàng triệu ràng buộc. Lập trình ràng buộc (constraint programming) là một lĩnh vực nghiên cứu tập trung vào việc phát triển các kỹ thuật để tìm ra giải pháp cho một tập hợp các ràng buộc với tốc độ cực nhanh hoặc chứng minh rằng không tồn tại giải pháp nào. Tôi là tác giả/đóng góp chính vào các trình giải như OpenWBO, OpenWBO-Inc, Shesha và CryptoMiniSAT.

Một blockchain có thể được hiểu như là việc thực thi của một máy trạng thái xác định (deterministic state machine). Việc thực hiện "thực thi" này theo cách phi tập trung và chịu lỗi (fault-tolerant) đòi hỏi kiến thức từ nghiên cứu về hệ thống phân tán. Tại Supra, chúng tôi đã phát triển DORA như một giao thức thỏa thuận oracle phân tán mới để thiết kế một oracle blockchain nhanh, có thể mở rộng, minh bạch và linh hoạt.

Bình luận

Tại Supra, tôi đã tham gia thiết kế một giao thức oracle rất linh hoạt, nhanh chóng, có thể mở rộng và minh bạch. Blockchain như một lĩnh vực nghiên cứu có rất nhiều điều thú vị vì nó có nhiều ứng dụng quan trọng trong thực tế. Chúng ta đã chứng kiến việc sử dụng blockchain trong tài chính và trò chơi. Một số chính phủ đã sử dụng blockchain như một sổ đăng ký không thể thay đổi để lưu trữ hồ sơ về tài sản bất động (ví dụ, đất đai) và tiền mã hóa của ngân hàng trung ương.

Tiềm năng của blockchain trong việc giảm thiểu các tranh chấp pháp lý trong nhiều giao dịch kinh doanh là không giới hạn. Nó có khả năng cho phép nhiều giao dịch kinh doanh giữa các bên mà không cần tin tưởng nhau trong khi thực thi các SLA đã thỏa thuận và các điều khoản nhằm thúc đẩy tốc độ diễn ra các giao dịch kinh doanh này. Cùng với những ứng dụng này, cần có giải pháp cho nhiều vấn đề nghiên cứu liên quan đến quyền riêng tư, đảm bảo công bằng.

Cố vấn

Tiến sĩ Saurabh Joshi đã hướng dẫn luận án cho nhiều sinh viên thạc sĩ và tiến sĩ tại IIT Hyderabad. Là một giảng viên, anh đã dạy các nguyên tắc của Ngôn ngữ lập trình, Giới thiệu về lập trình, Cơ sở phát triển phần mềm, Kỹ thuật phần mềm ở cấp độ đại học và Lập trình ràng buộc, Xác minh phần mềm ở cấp sau đại học.

Ấn phẩm nghiên cứu chọn lọc

Xem Trung Tâm Nghiên Cứu để biết thêm

2023

SupraTech

DORA: Thỏa thuận Oracle Phân tán với Đa số Đơn giản (Simple Majority)

với Prasanth Chakka, Tiến sĩ Aniket Kate, Joshua D. Tobkin and Tiến sĩ David Yang • 43rd IEEE International Conference on Distributed Computing Systems (ICDCS), 2023 • Đọc Litepaper

2019

Pinaka: Thực thi Biểu tượng Gặp gỡ Giải thuật Tăng dần

với (đồng tác giả) Một phần của Lecture Notes in Computer Science book series (LNTCS,volume 11429)

2017

Phân tích dự đoán chính xác để phát hiện tắc nghẽn giao tiếp trong các chương trình MPI

với (đồng tác giả) ACM Transactions on Programming Languages and Systems

2014

Ràng buộc Số lượng Tăng dần cho MaxSAT

với (đồng tác giả) Một phần của Lecture Notes in Computer Science book series (LNPSE,volume 8656)

2012

Khung kiểm thử không đầy đủ và lỗi xen kẽ

với (đồng tác giả) Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Tiềm năng của blockchain trong việc giảm thiểu các tranh chấp pháp lý trong nhiều giao dịch kinh doanh là không giới hạn. Nó có khả năng cho phép nhiều giao dịch kinh doanh giữa các bên mà không cần tin tưởng nhau trong khi thực thi các SLA đã thỏa thuận và các điều khoản nhằm thúc đẩy tốc độ diễn ra các giao dịch kinh doanh này. Cùng với những ứng dụng này, cần có giải pháp cho nhiều vấn đề nghiên cứu liên quan đến quyền riêng tư, đảm bảo công bằng.

Tiến sĩ Saurabh Joshi

Quyền riêng tưĐiều khoản sử sụngSử dụng dữ liệu và cookie trang webTiết lộ lỗiChính sách bảo mật thông tin sinh trắc học

©2024 Supra | Entropy Foundation (Thụy sĩ: CHE.383.364.961). Đã đăng ký Bản quyền