컴퓨터공학과 손병호 대학원생·배경민 교수, VMCAI 2026 Distinguished Paper Award 수상

컴퓨터공학과 손병호 대학원생(통합 ’22)과 배경민 교수가 1월 12일(월) 프랑스 렌(Rennes)에서 개최된 ‘27th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2026)’에서 ‘Distinguished Paper Award’를 수상했다.

VMCAI는 소프트웨어 및 시스템의 정형검증(Formal Verification), 모델체킹(Model Checking), 요약해석(Abstract Interpretation) 분야의 권위 있는 국제 학술대회로, 이론적 기반과 실제 시스템 검증 기술을 연결하는 연구 성과를 중점적으로 다루고 있다.

이번 학회에는 총 54편의 논문이 제출되어 이 중 18편이 채택되었으며, 상위 2편의 논문에만 ‘Distinguished Paper Award’가 수여됐다.

수상 논문의 제목은 ‘A Formal Executable Semantics of PROMELA’로, 분산 및 동시성 시스템의 정형 명세에 널리 활용되는 PROMELA 언어의 수학적 의미 구조를 기계적으로 실행 가능한 수준까지 정립한 연구이다. 특히, PROMELA 언어가 지니는 비결정성(nondeterminism)이나 원자성(atomicity) 등 고수준 선언적 특성을기계적 실행 모델에서 정교하고 일관되게 표현할 수 있는 의미론적 패턴 ‘Load-and-Fire’를 제안하였다. 이를 통해 기존에는 SPIN 모델체킹에 의존하여 제한된 범위에서만 분석이 가능했던 PROMELA 프로그램에 대한 코드 수준의 연역적 검증 가능성을 열었으며, 정형검증 연구의 이론적·방법론적 확장에 기여한 성과로 평가받았다.

이번 성과는 분산·동시성 시스템의 신뢰성 확보를 위한 정형기법 연구의 새로운 가능성을 제시한 것으로 평가되며, 우리 학과의 국제적 연구 경쟁력을 다시 한번 입증하는 계기가 됐다.