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