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Ý

Abstract

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.