Development of Practically Deployable Mechanized Specification-Based Automated Validation Technology for Software Correctness
개인기초연구(과기정통부)(R&D) · 우수연구-리더연구(유형A)
2026년
2710109727
과학기술정보통신부
한국연구재단
한국과학기술원
류석영
16명
2026.06.01 ~ 2027.02.28
2026.06.01 ~ 2035.02.28
5.9억원
5.9억원
기초연구
대학
대전광역시 유성구
정보/통신 > 정보이론 > 프로그래밍 언어/자연어 처리
본 연구과제의 최종 목표는 SW의 명세를 기계화하여 실행가능한 오라클과 테스트 및 자연어 명세를 자동으로 생성하여, SW의 품질을 획기적으로 향상시키는 것이다.
o 1년차: (1) 웹어셈블리 코드와 자바스크립트 코드 간 상호작용(WJI)의 의미와 양자 프로그래밍 언어인 OpenQASM의 의미 및 블록체인 이더리움 합의 알고리즘의 의미를 파악하여 명세를 기계화한다. (2) Python과 Rust 언어의 의미구조를 파악하고, 초소형 위성 펌웨어의 동작 의미구조를 파악한다.o 2년차: (1) WJI와 OpenQASM 및...
... 증가하고, 결함을 수정하는 데 드는 비용은 2년마다 21%씩 증가한다. 2025년 상반기 사이버 공격 신고 건수는 전년 동기 대비 15% 증가하여, 국내 대표적인 통신기업들이 정보보안에 7,000억원에서 ... 정의하고, 기계화된 명세로부터 올바름이 보장되는 구현체와 자연어 명세를 생성하여, SW 결함과 정보보안 비용을 획기적으로 줄일 수 있다.o 사회적 측면: SW가 사회적 인프라로서 점점 더 중요한 ...