Intereses y experiencia

Las metodologías de prueba convencionales, aunque son buenas en aplicaciones a gran escala, nunca pueden demostrar que un software está libre de errores. Los dominios de aplicación críticos, como la aviación, la exploración espacial, el transporte, la medicina y las finanzas, exigen que el software utilizado en ellos se adhiera estrictamente a la especificación. Los daños causados por un software con errores en estos dominios pueden provocar enormes pérdidas económicas o, en el peor de los casos, pueden causar varias víctimas mortales. El área de la verificación formal y los métodos formales se centra en el desarrollo de técnicas y herramientas que aseguren el máximo nivel de garantías de seguridad, esforzándose por asegurar y demostrar que el sistema subyacente no tiene ningún fallo. Empecé a explorar el área hace unas dos décadas como parte de mi investigación de máster.

Mientras las técnicas generales en la verificación formal constituyen la base para explorar el espacio de estados de un sistema en general, entender la semántica de los lenguajes de programación, los sistemas de tipos, el análisis de programas y los compiladores permite adaptar y perfeccionar estas técnicas para los sistemas de software. Lenguajes como Rust y Move buscan elevar la calidad del software con el principio de "más vale prevenir que curar", gracias a sus robustos sistemas de tipos. El paradigma de la programación funcional se está integrando y ganando popularidad en muchos lenguajes imperativos conocidos. Este diseño en los lenguajes de programación facilita enormemente el razonamiento automatizado sobre el software. He contribuido significativamente en varias herramientas de análisis de programas, verificación de software y reparación automática, incluyendo Pinaka, CBugs, AtomicInf, CBMC-Repair, 2LS, LLOV, GPURepair, entre otros.

Una blockchain puede interpretarse como la ejecución de una máquina de estados determinista. Realizar esta "ejecución" de forma descentralizada y tolerante a fallos requiere conocimientos procedentes de la investigación en sistemas distribuidos. En Supra, desarrollamos DORA como un novedoso protocolo de acuerdo de oráculo distribuido para diseñar un oráculo de blockchain rápido, escalable, transparente y resistente.

Comentario

En Supra, he participado en el diseño de un protocolo de oráculo altamente resistente, rápido, escalable y transparente. La blockchain como área de investigación tiene mucho que ofrecer, ya que tiene varias aplicaciones importantes en la vida real. Ya hemos sido testigos del uso de blockchain en las finanzas y los juegos. Algunos gobiernos ya están utilizando blockchains como registro inmutable para almacenar registros sobre bienes inmuebles (por ejemplo, terrenos) y monedas digitales del banco central.

El potencial de la blockchain para reducir los litigios en varias transacciones comerciales es ilimitado. Tiene el potencial de permitir varias transacciones comerciales entre partes que no se fían, al tiempo que hace cumplir los acuerdos de nivel de servicio y las condiciones acordadas, aumentando la velocidad a la que se realizan estas transacciones comerciales. Junto con estas aplicaciones, se necesitan soluciones a varios problemas de investigación relacionados con la privacidad y las garantías de imparcialidad.

tutoría

Saurabh Joshi ha sido tutor de varios estudiantes de máster y doctorado para sus tesis en el IIT de Hyderabad. Como miembro del profesorado, ha enseñado Principios de Lenguajes de Programación, Introducción a la Programación, Fundamentos del Desarrollo de Software, Ingeniería de Software a nivel de licenciatura y Programación con Restricciones, Verificación de Software a nivel de posgrado.

Selección de publicaciones de investigación