tailieunhanh - LUẬN VĂN:XÂY DỰNG HỆ THỐNG GIẢI BÀI TOÁN SMT HIỆU NĂNG CAO – PHẦN MÁY TRẠM

Vấn đề giải quyết các bài toán Satisfiability Modulo Theories (SMT) hiện nay đang được nghiên cứu và phát triển ở nhiều nơi trên thế giới. Cho đến ngày nay, nhiều trường đại học, tổ chức đã nghiên cứu và đưa ra những bộ giải giải quyết bài toán SMT (hay còn gọi là SMT solver). Ví dụ như Z3 của Mcrosoft, yices của SRI, CVC3 của một số trường đại học danh tiếng của Mỹ. hay boolector, openSMT của một số trường đại học danh tiếng khác . | ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Hoàng Thế Tùng XÂY DỰNG HỆ THỐNG GIẢI BÀI TOÁN SMT HIỆU NĂNG CAO - PHẦN MÁY TRẠM KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành Công nghệ phần mềm Cán bộ hướng dẫn TS. Trương Anh Hoàng Cán bộ đồng hướng dẫn TS. Phạm Ngọc Hùng HÀ NỘI - 2010 Xây dựng hệ thống giải bài toán SMT hiệu năng cao - Phần máy trạm 2010 Lời cảm ơn Trước hết tôi xin gửi lời cảm ơn chân thành và sâu sắc đến Tiến sỹ Trương Anh Hoàng và Tiến sỹ Phạm Ngọc Hùng những người đã trực tiếp hướng dẫn tôi trong suốt quá trình nghiên cứu và phát triển đề tài nghiên cứu này. Để có được những kết quả nghiên cứu như hiện nay tôi vô cùng biết ơn sự quan tâm hướng dẫn nhiệt tình của hai thầy trong thời gian vừa qua. Tôi xin chân thành cảm ơn các thầy cô trong trường Đại học công nghệ Đại học Quốc Gia Hà Nội nói chung và các thầy cô trong khoa công nghệ thông tin nói riêng những người đã nhiệt tình giảng dạy giúp tôi có những kiến thức quý báu để tôi có thể hoàn thành được đề tài luận văn này. Tôi xin bày tỏ lòng cảm ơn đến các anh chị cao học và các bạn trong nhóm nghiên cứu đã cùng tôi tìm hiểu và xây dựng hoàn chỉnh hệ thống giải quyết bài toán Satisfiability Modulo Theories SMT với hiệu năng cao giúp tôi có thể hoàn thành tốt phần nghiên cứu của mình. Và cuối cùng tôi xin gửi lời cảm ơn đến gia đình bạn bè và những người thân đã bên cạnh động viên giúp tôi hoàn thành tốt luận văn của mình. Hà Nội tháng 05 2010 Hoàng Thế Tùng Sinh viên Hoàng Thế Tùng - K51CNPM - Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD TS. Trương Anh Hoàng GVĐHD TS. Phạm Ngọc Hùng Xây dựng hệ thống giải bài toán SMT hiệu năng cao - Phần máy trạm 2010 Tóm tăt nội dung Vấn đề giải quyết các bài toán Satisfiability Modulo Theories SMT hiện nay đang được nghiên cứu và phát triển ở nhiều nơi trên thế giới. Cho đến ngày nay nhiều trường đại học tổ chức đã nghiên cứu và đưa ra những bộ giải giải quyết bài toán SMT hay còn gọi là SMT solver . Ví dụ như Z3 của Mcrosoft yices của SRI CVC3 của một số .