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.