兴趣和专长

传统的测试方法虽然适用于大规模应用，但永远不能证明一个软件是没有错误的。对于航空、太空探索、交通运输、医疗保健和金融等关键应用领域来说，要求在这些领域中使用的软件严格遵守规范。在这些领域中，一个有缺陷的软件可能导致巨大的财务损失，甚至在最坏的情况下可能导致人员死亡。形式验证和形式方法的领域专注于开发技术和工具，以确保并证明底层系统没有任何缺陷，从而提供最高级别的安全保证。我大约二十年前开始探索这个领域，并作为我硕士研究的一部分。

尽管形式验证领域内的通用技术为一般系统提供了状态空间探索的基础，但对编程语言语义、类型系统、程序分析和编译器的理解使人能够为软件系统采用和调整一些形式验证技术。Rust和Move等编程语言，借助其强大的类型系统，遵循“预防胜于治疗”的原则，致力于提高软件质量。函数式编程范式现在正在许多流行的命令式编程语言中得到采用和普及。这种编程语言设计原则对于自动推理软件非常有帮助。我在几个程序分析、软件验证和自动修复工具上做出了关键贡献，例如Pinaka、CBugs、AtomicInf、CBMC-Repair、2LS、LLOV、GPURepair等。

许多自动推理工具依赖于将程序表示为一组约束。这些约束的解通常可以映射到在执行过程中可能出现的bug上。如果约束的解不存在，则意味着没有错误存在。最先进的约束条件器（例如SAT/SMT求解器）能够处理数百万个约束。约束编程这一研究领域专注于开发技术，以极高的速度找到给定约束集的解，或者证明不存在解。我在OpenWBO、OpenWBO-Inc、Shesha和CryptoMiniSAT等求解器上做出了关键贡献。

区块链可以被看作是确定性状态机的执行。以分散的、容错的方式进行这种“执行”需要来自分布式系统研究的知识。在Supra，我们开发了DORA（分布式预言机协议）作为一种新颖的分布式预言机协议，旨在设计一个快速、可扩展、透明和弹性的区块链预言机。

评述

在Supra，我参与设计了一种高度弹性、快速、可扩展和透明的预言机协议。区块链作为一个研究领域有很多潜力，因为它在许多重要的现实生活应用中具有广泛的应用。我们已经看到了区块链在金融和游戏领域的应用。一些政府已经开始使用区块链作为不可更改的注册表，用于存储有关不动产（如土地）和中央银行数字货币的记录。

区块链在减少多种商业交易中的诉讼潜在风险方面具有巨大的潜力。它能够在执行协议和条款的同时，促成不信任各方之间的多个商业交易，从而加快这些交易的速度。除了这些应用，我们还需要解决与隐私和公平保障有关的多个研究问题。

导师经历

Dr. Saurabh Joshi在印度理工学院海得拉巴分校担任过多名硕士和博士生的学位论文导师。作为一名教职员，他承担了本科阶段的编程语言原理、编程导论、软件开发基础、软件工程等课程，以及研究生阶段的约束编程和软件验证等课程。

精选研究论文