Интересы и экспертиза

Традиционные методы тестирования, хотя и эффективны для крупных приложений, никогда не могут доказать, что программное обеспечение свободно от ошибок. Критически важные области применения, такие как авиация, космические исследования, транспорт, здравоохранение и финансы, требуют, чтобы используемое в этих областях программное обеспечение строго соответствовало спецификации. Ущерб, нанесенный ошибочным программным обеспечением в этих областях, может привести к огромным финансовым потерям, а в худшем случае — к многочисленным жертвам. Область формальной верификации и формальных методов сосредоточена на разработке техник и инструментов, чтобы обеспечить наивысший уровень гарантий безопасности, стремясь доказать, что базовая система не содержит ошибок. Я начал изучать эту область около двух десятилетий назад в рамках своей магистерской диссертации.

Хотя общие методы формальной верификации обеспечивают основу для исследования пространства состояний для общей системы, понимание семантики языков программирования, систем типов, анализа программ и компиляторов позволяет адаптировать некоторые методы формальной верификации для программных систем. Языки программирования, такие как Rust и Move, стремятся улучшить качество программного обеспечения, следуя принципу «Предупреждение лучше лечения» через свои сильные системы типов. Функциональное программирование сейчас активно внедряется и популяризируется в рамках многих популярных императивных языков программирования. Такие принципы разработки языков программирования значительно помогают в автоматизированных рассуждениях о программном обеспечении. Я был автором/внес ключевой вклад в разработку нескольких инструментов анализа программ/верификации программного обеспечения/автоматизированного исправления, таких как Pinaka, CBugs, AtomicInf, CBMC-Repair, 2LS, LLOV, GPURepair и другие.

Многие инструменты автоматизированного рассуждения полагаются на представление программы в виде набора ограничений. Решение этих ограничений часто можно сопоставить с ошибкой, которая может проявиться во время выполнения. Отсутствие какого-либо решения для ограничений означает отсутствие ошибок. Современные решатели ограничений (например, SAT/SMT-решатели) способны обрабатывать миллионы ограничений. Область программирования ограничений сосредоточена на разработке техник для поиска решения данного набора ограничений с высокой скоростью или доказательства того, что решение не существует. Я был автором/внес ключевой вклад в разработку решателей, таких как OpenWBO, OpenWBO-Inc, Shesha и CryptoMiniSAT.

Блокчейн можно рассматривать как выполнение детерминированной машины состояний. Выполнение этого «исполнения» в децентрализованной и отказоустойчивой манере требует знаний из области исследований распределенных систем. В Supra мы разработали DORA как новый протокол распределенного согласования оракулов для разработки быстрого, масштабируемого, прозрачного и устойчивого блокчейн-оракула."

Комментарий

В Supra я занимался разработкой высокоустойчивого, быстрого, масштабируемого и прозрачного протокола оракула. Блокчейн как область исследований предлагает много возможностей, так как он имеет несколько важных приложений в реальной жизни. Мы уже стали свидетелями использования блокчейна в финансах и играх. Некоторые правительства уже используют блокчейны как неизменяемый реестр для хранения данных об объектах недвижимости (например, земельные участки) и цифровых валютах центральных банков.

Потенциал блокчейна для сокращения судебных споров в бизнес-транзакциях безграничен. Он имеет потенциал для реализации множества бизнес-транзакций между ненадежными сторонами с соблюдением согласованных SLA и условий, что ускоряет процесс этих бизнес-транзакций. Наряду с этими приложениями требуются решения для ряда исследовательских задач, связанных с конфиденциальностью и гарантиями справедливости.

наставничество

Саураб Джоши наставлял нескольких магистров и докторантов по их дипломным работам в IIT Hyderabad. Как преподаватель, он преподавал Принципы языков программирования, Введение в программирование, Основы разработки программного обеспечения, Программную инженерию на уровне бакалавриата, а также Программирование ограничений, Верификацию программного обеспечения на уровне магистратуры.

Избранные научные публикации