Trong khoa học máy tính, phân tích chương trình là quá trình phân tích tự động hành vi của các chương trình phần mềm. Hai phương pháp tiếp cận trong phân tích chương trình là phân tích tĩnh và phân tích động. Phân tích chương trình được ứng dụng trong lĩnh vực đảm bảo sự đúng đắn của chương trình và tối ưu hóa chương trình phần mềm. Các kỹ thuật liên quan đến phân tích chương trình bao gồm: phân tích luồng điều khiển và luồng dữ liệu, phân tích dựa trên các ràng buộc, biểu diễn trừu tượng hóa, sử dụng các hệ thống kiểu. Trong các hệ thống phần mềm, lỗi phần mềm gây ra nhiều thiệt hại về kinh tế và con người, đặc biệt là những ứng dụng trong lĩnh vực ngân hàng, tài chính, điều khiển và kiểm soát các phương tiện, thiết bị giao thông, y tế... Vì vậy, việc đảm bảo chất lượng cũng như đảm bảo tính đúng đắn của phần mềm ngày càng trở nên quan trọng. Đã có nhiều phương pháp khác nhau đề xuất để tăng cường sự tin cậy cho phần mềm như kiểm chứng mô hình (model checking), kỹ thuật kiểm thử phần mềm và phân tích chương trình. Đề tài đề xuất các phương pháp mới để kiểm chứng các hệ thống phần mềm một cách hiệu quả sử dụng kỹ thuật phân tích chương trình. Phương pháp nghiên cứu của chúng tôi sẽ tái sử dụng các kỹ thuật ưu việt trong phân tích chương trình và xem xét để ứng dụng các kỹ thuật này trong lĩnh vực kiểm chứng phần mềm.