Tổng hợp chương trình là quá trình tự động xây dựng một chương trình máy tính tuân thủ một đặc tả hình thức cho trước. Trái ngược với các phương pháp xây dựng chương trình truyền thống như trình biên dịch, tổng hợp chương trình có thể tạo ra các chương trình không thể có được từ đặc tả chỉ bằng các phép biến đổi cú pháp. Khả năng này rất cần thiết khi xây dựng các chương trình hiệu quả cho phần cứng chuyên dụng với tập lệnh hạn chế hoặc khi sử dụng các đặc tả như ví dụ đầu vào-đầu ra. Tuy nhiên, không gian tìm kiếm lớn của các chương trình khả thi hạn chế khả năng mở rộng của tổng hợp chương trình trong thực tế. Luận văn này trình bày các kỹ thuật để tăng tốc quá trình tổng hợp chương trình của các chương trình vectơ bit không có vòng lặp, tối ưu theo một thước đo do người dùng định nghĩa. Các chương trình vectơ bit hoạt động trên các từ dữ liệu với số bit cố định. Các kỹ thuật được trình bày sẽ quyết định gần đúng xem một bài toán tổng hợp chương trình có bất khả thi hay không, tức là liệu một tập hợp các phép toán đã cho có đủ để xây dựng một chương trình thực hiện đặc tả hay không. Để làm được điều này, luận văn này khám phá các phương pháp để thu được sự phụ thuộc giữa các bit đầu vào và đầu ra của đặc tả và chuyển kiến ​​thức này sang phân tích các bài toán tổng hợp chương trình. Đánh giá các kỹ thuật được trình bày cho thấy chúng có thể giảm đáng kể thời gian cần thiết cho việc tổng hợp các chương trình vectơ bit tối ưu.

Abstract:

Program synthesis is the automatic construction of a computer program that adheres to a given formal specification. Contrary to traditional approaches to program construction such as compilers, program synthesis can create programs that cannot be obtained from the specification by syntactic transformations alone. This ability is essential when constructing efficient programs for specialized hardware with restricted instruction sets or when using specifications such as input-output examples. Unfortunately, the large search space of possible programs limits scalability of program synthesis in practice. This thesis presents techniques to accelerate program synthesis of loop-free bit vector programs that are optimal with respect to a user-defined metric. Bit vector programs operate on words of data with a fixed number of bits. The presented techniques approximately decide whether a program synthesis problem is unrealizable, that is whether a collection of given operations suffices to construct a program that implements the specification. To do this, this thesis explores approaches to obtain dependencies between the input and output bits of the specification and to transfer this knowledge to the analysis of program synthesis problems. An evaluation of the presented techniques shows that they can considerably reduce the time required for the synthesis of optimal bit vector programs

Ngôn ngữ:	eng
Tác giả:	Kamp, Marius
Thông tin nhan đề:	Detecting Unrealizable Bit Vector Program Synthesis Problems
Nhà xuất bản:	FAU University Press
Loại hình:	Tài nguyên giáo dục mở / Bộ sưu tập: Công nghệ thông tin
Bản quyền:	https://creativecommons.org/licenses/by/4.0/
Nguồn gốc:	OER
Mô tả vật lý:	261tr
Năm xuất bản:	2025