Reachability analysis is an approach to ensure software reliability by proving that a program cannot reach an unsafe state (e.g., an error location). Abstract Reachabiity-based Model Checking (ARMC) techniques conduct a reachability analysis in an abstraction of a program to mitigate the state-explosion problem. However, existing ARMC techniques are slow to detect a target path (i.e., a path reaching an error location) due to an inefficient search method. We propose a novel technique TOUR (effective error lOcation directed search via an interprocedUral Runtime distance calculation) to improve both bug detection ability and verification speed of ARMC by detecting a target path quickly. The key idea of TOUR is an error location directed search that utilizes the distance to an error location and function call context at runtime. TOUR applies four different distance metrics and a model for program-specific distance metric selection using static features of a program. We have extensively evaluated TOUR on 3,042 real-world C programs in a software verification competition benchmark. The experiment results show that TOUR, due to its error location directed search, finds bugs in 20\% more programs in 11\% less model checking time than the state-of-the-art ARMC technique (i.e., block-abstraction memoization) for 354 buggy programs. Also, TOUR verifies 15\% more programs within 15\% less model checking time than the block-abstraction memoization for 652 complex clean programs. In conclusion, TOUR achieves fast reachability analysis by speeding up ARMC, and the fast reachability analysis helps practitioners to efficient software reliability assurance.
추상 도달가능성 기반 모델 체킹 (ARMC)는 상태 폭발 문제를 피하기 위해 실제 프로그램 상태 공간을 추상화한 추상 상태 공간에서 도달가능성 분석을 수행한다. 그런데 기존 추상 도달가능성 기반 모델 체킹 기법들은 목표 경로에 도달하는데 오래 걸리는 문제가 있다. 본 연구에서는 목표 경로를 빨리 발견하여 ARMC의 결함 발견 능력과 검증 속도를 향상시키기 위해 TOUR라는 새로운 기법을 제안한다. TOUR는 실행 시간에 함수 호출 맥락과 에러 위치까지의 거리를 이용해서 에러 위치 지향 탐색을 수행하는 기법이다. TOUR는 네 가지 서로 다른 거리 기준을 이용하며 프로그램의 정적 특성들을 기반으로 거리 기준을 선택할 수 있다. 본 연구에서는 3,042개의 실제 C 프로그램들을 대상으로 TOUR를 엄밀하게 평가한다. 실험 결과 TOUR는 354개의 결함을 가진 프로그램들에 대해서 최신 ARMC 기법보다 20\% 많은 프로그램에서 11\% 적은 시간 만에 결함을 찾았다. 또한 TOUR는 652개의 복잡한 결함이 없는 프로그램들에 대해서 최신 ARMC 기법보다 15\% 많은 프로그램들을 15\% 적은 시간 만에 검증했다.
