관심사와 전문 지식

전통적인 테스트 방법론은 대규모 애플리케이션에서는 효과적이지만 소프트웨어가 결함이 없다는 것을 증명할 수는 없습니다. 항공, 우주 탐사, 운송, 헬스케어 및 금융과 같은 중요한 응용 분야에서는 이러한 분야에서 사용되는 소프트웨어가 사양을 엄격하게 준수해야 합니다. 이러한 분야에서 결함이 있는 소프트웨어로 인한 피해는 막대한 재정적 손실을 초래할 수 있으며, 최악의 경우 여러 사망자를 초래할 수 있습니다. 형식 검증 및 형식 방법 분야는 기본 시스템에 결함이 없음을 보장하고 증명하기 위해 최고 수준의 안전 보장을 보장하는 기술과 도구를 개발하는 데 중점을 둡니다. 저는 석사 연구의 일환으로 이 분야를 약 20년 전부터 탐구하기 시작했습니다.

형식 검증 내의 일반 기술은 일반 시스템에 대한 상태 공간 탐색의 기초를 제공하지만, 프로그래밍 언어의 의미론, 타입 시스템, 프로그램 분석 및 컴파일러에 대한 이해는 소프트웨어 시스템에 대해 일부 형식 검증 기술을 적용하고 수정하는 데 도움이 됩니다. Rust와 Move와 같은 프로그래밍 언어는 강력한 타입 시스템을 통해 “예방이 치료보다 낫다”는 원칙을 따르며 소프트웨어의 품질을 향상시키기 위해 노력하고 있습니다. 함수형 프로그래밍 패러다임은 현재 많은 인기 있는 명령형 프로그래밍 언어 내에서 채택되고 있습니다. 이러한 프로그래밍 언어 설계 원칙은 소프트웨어에 대한 자동 추론에 큰 도움이 됩니다. 저는 Pinaka, CBugs, AtomicInf, CBMC-Repair, 2LS, LLOV, GPURepair 등 여러 프로그램 분석, 소프트웨어 검증 및 자동 수리 도구에 대한 저자/핵심 기여를 했습니다.

많은 자동 추론 도구는 프로그램을 제약 조건 집합으로 표현하는 데 의존합니다. 이러한 제약 조건에 대한 솔루션은 종종 실행 중에 발생할 수 있는 결함에 매핑될 수 있습니다. 제약 조건에 대한 해결책이 없다는 것은 결함이 없다는 것을 의미합니다. 최첨단 제약 해결기(예: SAT/SMT 해결기)는 수백만 개의 제약 조건을 처리할 수 있습니다. 제약 프로그래밍은 주어진 제약 조건 집합에 대한 해결책을 극도로 빠르게 찾거나 해결책이 존재하지 않음을 증명하는 기술 개발에 중점을 둡니다. 저는 OpenWBO, OpenWBO-Inc, Shesha 및 CryptoMiniSAT와 같은 해결기에 대한 저자/핵심 기여를 했습니다.

블록체인은 결정론적 상태 기계의 실행으로 간주될 수 있습니다. 이러한 “실행”을 분산되고 내결함성이 있는 방식으로 수행하려면 분산 시스템 연구에 대한 지식이 필요합니다. Supra에서 우리는 빠르고 확장 가능하며 투명하고 회복력 있는 블록체인 오라클을 설계하기 위해 DORA라는 새로운 분산 오라클 합의 프로토콜을 개발했습니다.

코멘트

Supra에서 저는 고도로 회복력이 강하고 빠르며 확장 가능하고 투명한 오라클 프로토콜 설계에 참여하고 있습니다. 블록체인은 여러 중요한 실제 응용 프로그램을 가지고 있어 연구 분야로서 많은 가능성을 제공합니다. 우리는 이미 금융과 게임에서 블록체인 사용을 목격했습니다. 일부 정부는 불변의 레지스트리로 블록체인을 사용하여 부동산(예: 토지) 및 중앙은행 디지털 통화에 대한 기록을 저장하고 있습니다.

블록체인은 여러 비즈니스 거래에서 소송을 줄일 수 있는 잠재력이 무궁무진합니다. 블록체인은 신뢰하지 않는 당사자 간의 여러 비즈니스 거래를 가능하게 하면서 합의된 SLA 및 조건을 시행하여 이러한 비즈니스 거래가 이루어지는 속도를 높일 수 있는 잠재력을 가지고 있습니다. 이러한 응용 프로그램과 함께 프라이버시 및 공정성 보장과 관련된 여러 연구 문제에 대한 해결책이 필요합니다.

멘토십

Saurabh Joshi는 IIT 하이데라바드에서 석사 및 박사 학생들의 논문을 여러 차례 지도했습니다. 그는 교수로서 학부 과정에서 프로그래밍 언어의 원리, 프로그래밍 소개, 소프트웨어 개발 기초, 소프트웨어 공학을 가르쳤으며, 대학원 과정에서는 제약 프로그래밍 및 소프트웨어 검증을 가르쳤습니다.

선별 연구 발표 자료