Interests and expertise

Conventional testing methodologies, while good at large scale applications, can never prove that a software is free of bugs. Critical application domains such as aviation, space exploration, transport, healthcare, and finance demands that the software used in these domains adhere strictly to the specification. Damage caused by a buggy software in these domains can cause huge financial losses, or in the worst case, can cause several fatalities. Area of formal verification and formal methods focuses on developing techniques and tools to ensure highest level of safety guarantees by striving to ensure and prove that the underlying system does not have any bugs. I started exploring the area around two decades ago as a part of my masters research.

While general techniques within formal verification provides basis for state-space exploration for a general system, understanding of programming language semantics, type system, program analysis and compilers allow one to massage and adopt some of the formal verification techniques for software systems. Programming languages such as Rust and Move strive to improve the quality of software by following the principle of “Prevention is better than cure” through their strong type systems. Functional programming paradigm is now being adopted and popularized within many popular imperative programming langauges. Such programming language design principle aid greatly in automated reasoning about software. I have authored/made key contributions on several program analysis/software verification/automated repair tools such as Pinaka, CBugs, AtomicInf, CBMC-Repair, 2LS, LLOV, GPURepair, etc.

Many of the automated reasoning tools rely on representing a program as a set of constraints. Solution to these constraints can often be mapped to a bug that may manifest during execution. Absence of any solution to the constraints imply the absence of any bugs. State-of-the-art constraint solvers (e.g., SAT/SMT solvers) are capable of handling millions of constraints. Constraint programming as a research area focuses on developing techniques of finding a solution to a given set of constraints with extreme speed or proving that no solution exists. I have authored/made key contributions on solvers such a OpenWBO, OpenWBO-Inc, Shesha, and CryptoMiniSAT.

A blockchain can be construed as an execution of a deterministic state machine. Doing this “execution” in a decentralized and fault-tolerant manner requires knowledge from distributed systems research. At Supra, we developed DORA as a novel distributed oracle agreement protocol to design a fast, scalable, transparent and resilient blockchain oracle.

Commentary

At Supra, I have been involved in designing a highly resilient, fast, scalable and transparent oracle protocol. Blockchain as a research area has a lot to offer since it has several important real-life applications. We have already witnessed blockchain usage in finance and gaming. Some governments are already using blockchains as an immutable registry for storing records about immovable properties (e.g., land) and central-bank digital currencies.

The potential of blockchain to reduce litigations in several business transactions is limitless. It has the potential to enable several business transactions between untrusting parties while enforcing agreed-upon SLAs and terms boosting the speed at which these business transactions take place. Along with these applications, solutions to several research problems dealing with privacy, fairness guarantees are required.

mentorship

Saurabh Joshi has mentored several masters and PhD student for their theses at IIT Hyderabad. As a faculty member, he has taught Principles of Programming Languages, Introduction to Programming, Software Development Fundamentals, Software Engineering at undergraduate level and Constraint Programming, Software Verification at postgraduate level.

Selected research publications