Bài viết Kiểm chứng chương trình dựa trên sinh điều kiện kiểm chứng và chứng minh định lý trình bày một cách tiếp cận kiểm chứng phần mềm dựa trên hai kỹ thuật sinh điều kiện kiểm chứng và kỹ thuật hình thức chứng minh định lý tự động. | Kỷ yếu Hội nghị Quốc gia lần thứ VIII về Nghiên cứu cơ bản và ứng dụng Công Nghệ thông tin (FAIR); Hà Nội, ngày 9-10/7/2015 KIỂM CHỨNG CHƯƠNG TRÌNH DỰA TRÊN SINH ĐIỀU KIỆN KIỂM CHỨNG VÀ CHỨNG MINH ĐỊNH LÝ Nguyễn Ngọc Cương1, Nguyễn Trường Thắng2, Trần Mạnh Đông2 1 Khoa Toán - Tin học, Học viện An ninh nhân dân 2 Viện Công nghệ thông tin, Viện Hàn lâm Khoa học và Công nghệ Việt Nam , ntthang@, dongtm@ TÓM TẮT - Phần mềm ngày càng đóng vai trò rất quan trọng trong hầu hết các lĩnh vực của đời sống xã hội. Từ những trang thông tin điện tử, các hệ thống quản lý nghiệp vụ ngân hàng, các thiết bị di động, các thiết bị y tế, đến các thiết bị gia dụng sử dụng hàng ngày Ở đâu cũng có sự góp mặt của phần mềm. Tuy nhiên, phát triển và bảo trì phần mềm ngày cảng trở nên phức tạp và tốn rất nhiều chi phí. Sự phức tạp và chi phí có thể được giảm nếu trong pha phát triển phần mềm công việc kiểm chứng chương trình được thực hiện bên cạnh đó. Bài báo này trình bày một cách tiếp cận kiểm chứng phần mềm dựa trên hai kỹ thuật sinh điều kiện kiểm chứng và kỹ thuật hình thức chứng minh định lý tự động. Từ khóa - Phương pháp hình thức, kiểm chứng chương trình, chứng minh định lý, điều kiện kiểm chứng. I. GIỚI THIỆU Trong cuộc cách mạng công nghệ thông tin (CNTT) trên thế giới hiện nay, phần mềm là cốt lõi, chiếm tỷ trọng và vai trò ngày càng lớn trong nền kinh tế. Chính vì xu thế này, sự phụ thuộc ngày càng tăng của hoạt động kinh tế-xã hội vào chất lượng phần mềm. Tuy nhiên, có một thực tế là phần mềm và quy trình phát triển phần mềm ngày càng trở nên phức tạp và đắt đỏ. Nguyên nhân là do ngày càng có nhiều yêu cầu khắt khe đặt ra cho phần mềm, gồm các yêu cầu chức năng và phi chức năng. Do vậy, yêu cầu bức thiết của ngành công nghiệp phần mềm hiện đại là việc kiểm soát chất lượng phần mềm. Các phương pháp kiểm chứng phần mềm hình thức (formal software verification) là một trong những kỹ thuật đang được giới nghiên cứu cũng như giới công .
