Towards Efficient Function Abstraction via Active Learning for Property Falsification : 속성 변조를 위한 능동적 학습을 통한 효율적인 함수 추상화를 위해

국문 초록 (Abstract)

소프트웨어 프로그램의 속성 변조는 종종 상태 공간 폭발로 인해 제약을 받기 때문에 복잡한 시스템을 효율적으로 분석하는 것이 어렵습니다. 이 논문은 C 프로그램의 상태 기반 추상화를 생성하기 위해 능동 학습을 사용하는 방법을 조사하며, 목표 속성에 대한 정확성을 유지하면서 변조 비용을 줄이는 것을 목표로 합니다. 제안된 접근 방식은 속성 기반 함수와 변수 선택을 반복적이고 반례 기반의 능동 학습 절차와 통합합니다. 실행 추적을 사용하여 후보 상태 기반 모델을 생성하고, 이 모델은 완전성 검사와 반례 분석을 통해 정제됩니다. 최종 모델은 추상화된 C 함수로 변환되어 원래 프로그램에 다시 통합되어 속성 변조에 적합한 간소화된 버전을 생성합니다. SV-COMP 제품군의 벤치마크 프로그램에 대한 실험 결과, 제안된 추상화 접근 방식이 검증 시간과 메모리 소비를 상대적으로 줄인다는 것을 보여줍니다. 이 연구는 속성 변조를 위한 건전하고 속성 지향적인 접근 방식을 제공하는 능동 학습 기반 함수 추상화를 위한 새로운 프레임워크를 제공합니다. 결과는 추상화를 위해 능동 학습을 활용하는 것이 복잡한 소프트웨어 시스템을 효율적으로 검증하는 데 유망한 방향임을 시사합니다.

목차 (Table of Contents)

• 1 Introduction 1
• 1.1 Motivation 1
• 1.2 Approach 4
• 1.3 Thesis Structure 6
• 2 Background 7
• 2.1 Bounded Model Checking 7
• 2.2 Abstraction 10
• 2.3 Dependency Analysis 11
• 2.4 Active Learning 14
• 2.4.1 Basic Concept 14
• 2.4.2 Active Learning Using Model Checking as a Teacher 16
• 3 Property-Dependent Function Abstraction using Active Learning 19
• 3.1 Overview 19
• 3.2 Property-based function via dependency analysis 21
• 3.3 State machine generation using Active Learning 26
• 3.4 State Machine to C 29
• 4 Experiment 30
• 4.1 Experiment Set-up 30
• 4.2 Benchmark Programs 30
• 4.3 Experiment Procedure 31
• 4.4 Results and Analysis 32
• 5 Related Work 37
• 5.1 Function Summaries and Selective Abstraction 37
• 5.2 Compositional Model Checking 38
• 6 Limitation 39
• 7 Conclusion 40
• References 41
• Korean Abstract 46