[논문] 매칭 로직 속성의 구문 기반 점진적 프로그램 검증

출처: arXiv - 2606.08824v1

개요

증분성은 대규모·장수 소프트웨어 시스템의 복잡성을 정복하기 위한 기본 설계 원칙입니다. 이 원칙은 애자일 개발 프로세스에 채택되어 지속적인 소프트웨어 진화의 기반이 되고 있습니다. 이 맥락에서 주요 과제는 모든 변경 후에 소프트웨어 아티팩트의 정확성을 증분적으로 재검증하는 것으로, 검증 작업을 변경에 영향을 받은 부분에만 집중시키는 것입니다. 우리는 매칭 로직으로 표현된 속성으로 주석이 달린 KernelC 프로그램에 대한 증분 검증 접근법을 제시합니다. 이 접근법은 구문‑의미론적 프레임워크에 기반하여 코드 조각을 독립적으로 분석할 수 있게 하며, 프로그램 조각이 변경된 후에는 의미가 영향을 받은 부분만 다시 처리합니다. 이러한 특성은 연산자 우선순위 문법을 통해 언어 구문을 표현하고, 합성된 속성 스키마를 통해 의미를 형식화함으로써 얻어집니다. 우리는 이 기술을 프로토타입 도구에 구현하고 실험적으로 효율성을 평가했습니다. 결과는 우리 접근법이 형식 검증의 효율성을 저하시키지 않으며, 주석의 존재·유형, 변경 위치 및 프로그램 구조에 따라 변경 후 프로그램 재검증보다 더 나은 성능을 보일 수 있음을 보여줍니다.

핵심 기여

이 논문은 다음 분야의 연구를 제시합니다.

• cs.SE

방법론

자세한 방법론은 전체 논문을 참고하십시오.

실용적 시사점

본 연구는 cs.SE 분야의 발전에 기여합니다.

저자

• Domenico Bianculli
• Antonio Filieri
• Carlo Ghezzi
• Dino Mandrioli
• Alessandro Maria Rizzi

논문 정보

• arXiv ID: 2606.08824v1
• 분류: cs.SE
• 게시일: 2026년 6월 7일
• PDF: PDF 다운로드