• 목록

컴퓨터학부 소속 김요엘 박사과정생(지도교수: 최윤자)이 2026년 7월 5일-9일에 캐나다 몬트리올에서 개최되는 FSE 2026에 채택되었다.

- 논문 제목: Active Learning of Symbolic Automata for Reactive Programs via Dynamic Symbolic Mapper

- 저자 정보: 김요엘 (제 1저자), 최윤자 (교신저자)

- 학회 홈페이지: https://conf.researchr.org/home/fse-2026

FSE (ACM International Conference on the Foundations of Software Engineering)는 ICSE, ASE와 더불어 소프트웨어공학 분야 세계 최고 권위의 학술대회로 널리 인정받고 있으며, 국내에서도 BK21 최우수 국제학술대회 (인정 IF 최고 등급인 4)로 지정되어 있다. 이번 FSE 2026에는 총 920편의 논문이 제출되었으며, 이 중 88편이 major revision 없이 즉시 게재 수락을 받았고, 133편의 major revision invitation 중 최종 123편이 게재 수락을 받으며 약 22.9% (211/920)의 게재 수락률을 보였다. 김요엘 박사과정생은 지난 FSE 2024에 이어 두 번째 FSE 논문을 게재하게 되었으며, 이는 최윤자 교수가 이끄는 소프트웨어안전공학 연구실이 소프트웨어공학 분야의 최신 연구 흐름 속에서 꾸준히 경쟁력 있는 연구 성과를 축적해 왔음을 보여준다는 점에서 의미가 크다.

오토마타 학습(automata learning)은 소스코드로부터 프로그램의 중요한 행위 정보를 담은 오토마타를 학습하는 소프트웨어 역공학(software reverse engineering) 분야의 한 축이다. 학습된 오토마타는 원본 프로그램의 모형(model)으로 활용될 수 있으며, 이러한 모형은 모형을 검증하여 원본 프로그램의 신뢰성을 높이는 모형 검증(model checking), 모형으로부터 프로그램 명세를 추출하는 스펙 마이닝(specification mining), 그리고 모형으로부터 테스트를 생성하는 모델 기반 테스팅(model-based testing) 등에 주로 사용된다.

본 연구는 기존 오토마타 학습 기법의 병목 원인 중 하나인, 많은 프로그램 변수와 다양한 값 도메인(enum, integer, float 등)을 함께 다루어야 하는 문제를 불리언 추상화(Boolean abstraction)를 통해 해결하고, 이를 바탕으로 불리언 벡터 공간에서의 오토마타 학습을 가능하게 하는 기법을 제안한다. 구체적으로, 오토마타를 능동 학습(active learning)하는 과정에서 학습자(learner)와 교사(teacher) 사이에 매퍼(mapper) 컴포넌트를 삽입하여, 원래의 복잡한 프로그램 상태와 입출력을 불리언 벡터 형태로 추상화한 뒤 이를 바탕으로 학습이 이루어지도록 한다.

제안한 기법의 효과성은 차량, 로봇, 엘리베이터, 드론, 인공위성 제어 프로그램 등 다양한 임베디드 소프트웨어를 대상으로 한 실험을 통해 검증하였다. 그 결과, 기존 기법 대비 동일한 시간 내에 더 많은 오토마타를 학습하였으며(총 120개 벤치마크 중 32개 추가 학습), 학습 속도 또한 평균 55.6% 향상됨을 확인함으로써 제안 기법의 실용성을 입증하였다.

논문 초록:

Active learning of formal behavior models from program source code is a powerful approach to support a wide range of software analysis, validation, and verification tasks, for example, understanding system intent, automating specification mining, generating test oracles, and checking formal properties. Recent advances in active learning of symbolic automata, powered by program synthesis and model checking, provide both rich expressiveness and soundness guarantees for the learned models. However, these techniques often encounter significant performance bottlenecks, particularly when dealing with reactive programs that expose many program variables spanning large value domains. This work introduces an extended active learning algorithm tailored for reactive programs by incorporating a novel dynamic symbolic mapper for learning symbolic automata. The mapper abstracts program behavior using predicates over program variables inferred by the learner, encodes each valuation of these variables as a Boolean vector induced by these predicates (Boolean abstraction), and dynamically refines the abstraction in response to missing behaviors revealed by the teacher. It is granularity-aware: for teaching, it employs the coarsest predicates sufficient to expose missing behaviors, enabling broad exploration; for learning, it refines only to the finest predicates necessary to resolve the uncovered gaps, trying to minimize the number of refinements that could have been triggered by coarse abstraction. We evaluated our approach on 120 benchmarks, including SV-COMP tasks, Simulink model-driven programs, LeetCode problems, and representative embedded control software. The results show that our method learns 32 more symbolic automata and reduces the average active learning time by 55.6% compared to the state-of-the-art.