Computer Aided Verification
Cập nhật vào: Thứ tư - 19/11/2025 21:07
Nhan đề chính: Computer Aided Verification
Nhan đề dịch: Xác minh có hỗ trợ máy tính
Tác giả: Arie Gurfinkel, Vijay Ganesh
Nhà xuất bản: Springer Cham
Năm xuất bản: 2024
Số trang: 455 tr.
Ngôn ngữ: Tiếng Anh
ISBN: 978-3-031-65630-9
SpringerLink
Lời giới thiệu: Cuốn sách là phần II của kỷ yếu hội nghị CAV 2024 (Computer Aided Verification), tổng hợp các bài báo nghiên cứu mới nhất trình bày tại hội nghị này. CAV (Conference on Computer-Aided Verification) là hội nghị quốc tế hàng đầu về xác minh phần mềm và hệ thống, nơi các nhà nghiên cứu trình bày các kỹ thuật, công cụ và lý thuyết tiên tiến nhằm đảm bảo tính đúng đắn và tin cậy của hệ thống máy tính. Phần này của kỷ yếu gồm các chủ đề lớn sau:
+ Concurrency (Đồng thời): Các phương pháp xác minh chương trình đa luồng, giảm phạm vi kiểm tra và các kỹ thuật tối ưu hóa trong xác minh hệ thống song song.
+ Distributed Systems (Hệ thống phân tán): Xác minh các hệ thống hoạt động phân tán, logic bậc nhất, các mô hình chuyển tiếp, và các công cụ hỗ trợ. SpringerLink
+ Runtime Verification & Monitoring (Xác minh khi chạy và giám sát): Kỹ thuật để theo dõi hệ thống khi vận hành thực tế, dự đoán vi phạm, thực thi kiểm tra trong thời gian thực.
+ Case Studies & Tools (Nghiên cứu thực tế & công cụ): Các bài toán thực tế như giám sát máy bay không người lái, chuyển đổi hệ thống tín hiệu đường sắt, tính trách nhiệm pháp lý trong hệ thống tự động, và các công cụ hỗ trợ xác minh.
+ Machine Learning & Neural Networks (Học máy & mạng nơ-ron): Xác minh mạng nơ-ron, xây dựng bộ giám sát cho hệ thống AI, phân tích tính an toàn khi kết hợp AI và hệ thống phần mềm.
Từ khóa: Khoa học máy tính; Ứng dụng; Học máy; Tin học
Nội dung cuốn sách gồm những phần sau:
Tính đồng thời:
- Công cụ xác minh VerCors: Báo cáo tiến độ
- Giảm thứ tự bộ phận động tối ưu tiết kiệm
- Hợp đồng tập thể cho các chương trình song song truyền thông điệp
Hệ thống phân tán:
- mypyvy: Một nền tảng nghiên cứu để xác minh hệ thống chuyển đổi trong logic bậc nhất
- Triển khai hiệu quả miền trừu tượng của các công thức bậc nhất có lượng từ
- Xác minh việc “cắt bánh”, nhanh hơn
Xác minh và giám sát thời gian chạy:
- Xác minh thời gian chạy dự đoán tổng quát
- Thực thi bậc nhất chủ động theo thời gian thực
- Giám sát dự đoán với tiền tố vết mạnh
Các nghiên cứu điển hình và công cụ:
- Giám sát máy bay không người lái: Đặc tả, tích hợp và bài học kinh nghiệm
- Kiểm tra quá trình chuyển đổi từ hệ thống liên động đường sắt tương tự sang hệ thống liên động đường sắt dựa trên phần mềm
- soid: Một công cụ để truy cứu trách nhiệm pháp lý đối với việc ra quyết định tự động
Học máy và mạng nơ-ron:
- Marabou 2.0: Một công cụ phân tích hình thức đa năng cho mạng nơ-ron
- Monitizer: Tự động hóa thiết kế và đánh giá các bộ giám sát mạng nơ-ron
- Hướng dẫn tổng hợp chương trình liệt kê bằng các mô hình ngôn ngữ lớn
- Nâng cao tổng hợp đặc tả chương trình bằng các mô hình ngôn ngữ lớn sử dụng phân tích tĩnh và xác minh chương trình
- Xác minh thuộc tính an toàn kép toàn cục trong mạng nơ-ron với độ tin cậy cao
- Độ chính xác mạnh mẽ được chứng nhận của mạng nơ-ron bị giới hạn do lỗi Bayes
- Nâng cao xác minh tính mạnh mẽ với ít điểm ảnh thông qua các thiết kế xác minh bao phủ
- Thống nhất xác minh an toàn định tính và định lượng của hệ thống điều khiển bằng mạng nơ-ron sâu.
Liên hệ
Tiếng Việt
Tiếng Anh








