Thạc Sĩ Kiểm chứng chương trình dựa trên SMT

iii

MỤC LỤC
LỜI CAM ĐOAN i
LỜI CẢM ƠN . ii
MỤC LỤC . iii
BẢNG CÁC THUẬT NGỮ VIẾT TẮT v
DANH MỤC HÌNH VẼ . vi
Chương 1. GIỚI THIỆU 1
1.1. Đảm bảo chất lượng phần mềm 1
1.2. Mục tiêu của luận văn . 2
1.3. Nội dung luận văn 2
Chương 2. KIỂM CHỨNG CHƯƠNG TRÌNH VÀ THỰC THI TƯỢNG
TRƯNG . 3
2.1. Kiểm chứng chương trình . 3
2.1.1. Tổng quan về kiểm chứng chương trình 3
2.1.2. Kiểm chứng mô hình 4
2.2. Thực thi tượng trưng . 8
2.2.1. Tổng quan về thực thi tượng trưng 9
2.2.2. Kỹ thuật thực thi tượng trưng động . 13
2.2.3 Thực thi tượng trưng động và giải pháp 17
Chương 3. SATISFIABILITY MODULO THEORIES (SMT) . 20
3.1 SAT solver 20
3.1.1 Bài toán SAT . 20
3.1.2 Thuật toán DPLL cho SAT 21
3.2 SMT solver 26
3.3.1 Bài toán của SMT 26
3.3.2 Thuật toán DPLL cho SMT 28
3.2.3 SMT solver Boolector, Z3, và STP 29
Chương 4. KIỂM CHỨNG DỰA TRÊN KLEE . 39
4.1. Giới thiệu về khung làm việc của KLEE 39
4.1.1. Đầu vào của KLEE . 41 iv

4.4.2. Tối ưu hóa tập các ràng buộc với KLEE . 42
4.1.3. Giải ràng buộc tự động với metaSMT . 45
4.2. Độ bao phủ mã nguồn của ca kiểm thử được sinh bởi KLEE . 49
4.3. Thực thi tương trưng động với KLEE 55
4.4. Thực thi tượng trưng động và giải pháp của KLEE 56
4.5. Một số bài toán kiểm chứng và kiểm thử tự động dựa trên KLEE 57
4.3.1. Kiểm tra lỗi chia cho 0 trong chương trình . 57
4.3.2. Phát hiện lỗi truy cập ra ngoài kích thước của mảng . 59
4.3.3. Phát hiện lỗi hàm khi đột ngột gọi hàm abort . 62
4.3.4. Sinh dữ liệu kiểm thử tự động . 63
KẾT LUẬN . 69