Đề tài nghiên cứu phương pháp sinh dữ liệu kiểm thử một cách tự động dựa trên kỹ thuật thực thi tượng trưng (Symbolic execution) và công cụ SMT solver. Phương pháp sinh dữ liệu kiểm thử tự động này được áp dụng cho bài toán kiểm chứng các tính chất của chương trình, tìm ra các bộ dữ liệu kiểm thử vi phạm các tính chất cần kiểm chứng của chương trình (assertions). Đề xuất phương pháp sinh dữ liệu kiểm thử dựa trên việc phân tích dữ liệu đầu vào mang thông tin (sensitive data), kỹ thuật này áp dụng để cải tiến module sinh dữ liệu kiểm thử trong SMT solver raSAT, một công cụ SMT solver do chủ trì đề tài xây dựng và phát triển. Xây dựng bộ công cụ phần mềm để kiểm chứng một số tính chất của chương trình phần mềm dựa trên kỹ thuật thực thi tượng trưng và SMT solver. Tiến hành thực nghiệm trên công cụ phần mềm để đánh giá tính hiệu quả của các phương pháp đề xuất và công cụ xây dựng trên bộ dữ liệu chuẩn thực nghiệm chuẩn SV-Comp (Software Verification Competition). Tích hợp và áp dụng công cụ đã xây dựng về kiểm thử và kiểm chứng tự động; các phương pháp và kỹ thuật thực thi tượng trưng (SE), bộ giải SMT solver trong các bài toán về kiểm chứng, kiểm thử tự động khác. Hướng tới xây dựng nhóm nghiên cứu về các phương pháp sinh dữ liệu kiểm thử tự động cho phần mềm dựa trên kỹ thuật thực thi tượng trưng và các công cụ SMT solver để giải quyết các bài toán về sinh dữ liệu kiểm thử tự động, kiểm chứng các tính chất của mã nguồn, tự động tìm lỗi, ... của chương trình phần mềm. Trên cơ sở đó, xây dựng các bộ công cụ sinh dữ liệu kiểm thử tự động ứng dụng trong sản xuất phần mềm.