Tools and Algorithms for the Construction and Analysis of Systems (Part II)

Cập nhật vào: Thứ hai - 31/07/2023 16:11

Nhan đề chính: Tools and Algorithms for the Construction and Analysis of Systems (Part II)

Nhan đề dịch: Công cụ và thuật toán để xây dựng và phân tích hệ thống (Tập II)

Tác giả: Sriram Sankaranarayanan, Natasha Sharygina

Nhà xuất bản: Springer Cham

Năm xuất bản: 2023

Số trang: XXIV, 604 tr.

Ngôn ngữ: Tiếng Anh

ISBN: 978-3-031-30820-8

SpringerLink

Lời giới thiệu: Cuốn sách truy cập mở này là biên bản của Hội nghị quốc tế lần thứ 29 về công cụ và thuật toán để xây dựng và phân tích hệ thống, TACAS 2023, được tổ chức như một phần của Hội nghị chung châu Âu về lý thuyết và thực hành phần mềm, ETAPS 2023, vào ngày 22 tháng 4 -27, 2023, tại Paris, Pháp. 56 bài báo đầy đủ và 6 bài trình diễn công cụ ngắn được trình bày trong tập này đã được xem xét và lựa chọn cẩn thận từ 169 bài nộp.

Kỷ yếu cũng bao gồm 1 bài nói chuyện, 13 bài báo của cuộc thi liên kết SV-Comp và 1 bài báo bao gồm báo cáo cuộc thi.

TACAS là diễn đàn dành cho các nhà nghiên cứu, nhà phát triển và người dùng quan tâm đến các công cụ và thuật toán dựa trên cơ sở chặt chẽ để xây dựng và phân tích hệ thống. Hội nghị nhằm mục đích thu hẹp khoảng cách giữa các cộng đồng khác nhau có chung mối quan tâm này và hỗ trợ họ trong nỗ lực cải thiện tiện ích, độ tin cậy, tính linh hoạt và hiệu quả của các công cụ và thuật toán để xây dựng các hệ thống do máy tính điều khiển.

Từ khóa: Khoa học máy tính; Tin học; Nghiên cứu; Ứng dụng; Kỷ yếu.

Nội dung cuốn sách gồm những phần sau:

- EVA: Công cụ để xác minh thành phần của các mô hình AUTOSAR

- WASIM: Khung mô phỏng biểu tượng trừu tượng cấp độ từ để xác minh chính thức phần cứng

- Nhập phiên nhiều bên trong Java, suy luận

- PyLTA: Công cụ xác minh cho các thuật toán phân tán được tham số hóa

- FuzzBtor2: Trình tạo ngẫu nhiên các vấn đề kiểm tra mô hình cấp độ từ ở định dạng Btor2

- Eclipse ESCET™: Bộ công cụ kỹ thuật điều khiển giám sát của Eclipse

- Tối ưu hóa tổ hợp/Chứng minh định lý

- Các thuật toán tập hợp theo hướng dẫn cốt lõi và mới để tối ưu hóa tổ hợp đa mục tiêu

- Mức giảm đã được xác minh để tối ưu hóa

- Chỉ định và xác minh Trình lặp Rust bậc cao hơn

- Mở rộng Trình chứng minh hiệu suất cao sang Logic bậc cao hơn

- Công cụ (Giấy tờ thông thường)

- Nguyên mẫu WhyRel để xác minh quan hệ mô-đun của các chương trình con trỏ

- Kết nối phân tích phần cứng và phần mềm với Btor2C: Trình dịch từ cấp độ mạch sang C

- CoPTIC: Lập trình ràng buộc được dịch sang C

- Acacia-Bonsai: Một triển khai hiện đại về khả năng hiện thực hóa LTL dựa trên suy thoái

- Tính toán các giả định cho phép đầy đủ để tổng hợp

- Tổng hợp bộ điều khiển có lập trình hướng dẫn xác minh

- Điều chỉnh các giới hạn lớn trong tổng hợp từ các thông số kỹ thuật về sự sống có giới hạn

- Thành phần Lockstep cho các vòng lặp không cân bằng

- Tổng hợp các hệ thống dựa trên thỏa thuận phân tán với xác minh có thể quyết định hiệu quả

- Tổng hợp phản ứng LTL với một vài gợi ý

- Xác minh và tổng hợp Automata theo thời gian thông qua Học Automata hữu hạn

- Đồ thị/Hệ xác suất

- Thuật toán thời gian tuyến tính thực sự mang tính biểu tượng cho phân tách SCC

- Chuyển đổi các công thức Boolean đã định lượng bằng Biclique Covers

- Chứng chỉ cho Máy tự động đẩy xuống xác suất thông qua phép lặp giá trị lạc quan

- Xác minh chương trình xác suất thông qua tổng hợp quy nạp các bất biến quy nạp

- Giám sát thời gian chạy/Phân tích chương trình

- Thử nghiệm đồng thời được kiểm soát theo cường độ công nghiệp cho với C#

- Các hệ thống siêu ràng buộc nhạy cảm theo ngữ cảnh để phân tích chương trình có thể giải thích được

- Giám sát trực tuyến có thể giải thích được về logic thời gian số liệu

- Cuộc thi lần thứ 12 về Xác minh phần mềm — SV-COMP 2023

- Cạnh tranh về Xác minh Phần mềm và Xác thực Nhân chứng: SV-COMP 2023

- Symbiotic-Witch 2: Thuật toán hiệu quả hơn và Bác bỏ nhân chứng

- 2LS: Mảng và gỡ vòng lặp

- Bubaak: Giám sát thời gian chạy của trình xác minh chương trình

- Cuộc thi lần thứ 12 về Xác minh phần mềm - SV-COMP 2023

EBF 4.2: Xác minh hợp tác hộp đen cho các chương trình đồng thời

- Tự động giải thích trừu tượng mô-đun chủ đề

- Java: Hỗ trợ các thao tác chuỗi và mảng trong Java

- Korn -Xác minh phần mềm với các điều khoản Horn

- Mopsa-C: Miền mô-đun và Diễn giải trừu tượng quan hệ cho các chương trình C

- PIChecker: Trình xác minh dựa trên POR và Nội suy cho các chương trình đồng

- Ultimate Automizer và Dạng chuẩn CommuHash

- Ultimate Taipan và Phát hiện chủng tộc trong Ultimate

- VeriAbsL: Xác minh có thể mở rộng bằng cách trừu tượng hóa và dự đoán chiến lược

- VeriFuzz 1.4: Kiểm tra (Không) chấm dứt

Tools and Algorithms for the Construction and Analysis of Systems (Part II)

Những tin mới hơn

Những tin cũ hơn