Detecting Unrealizable Bit Vector Program Synthesis Problems
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 transfor...
Wedi'i Gadw mewn:
| Prif Awdur: | |
|---|---|
| Fformat: | Online |
| Iaith: | Saesneg |
| Cyhoeddwyd: |
FAU University Press
2025
|
| Pynciau: | |
| Mynediad Ar-lein: | ONIX_20251215T160703_9783961477944_9 |
| Tagiau: |
Dim Tagiau, Byddwch y cyntaf i dagio'r cofnod hwn!
|
| _version_ | 1869520637780819968 |
|---|---|
| author | Kamp, Marius |
| author_browse | Kamp, Marius |
| author_facet | Kamp, Marius |
| author_sort | Kamp, Marius |
| collection | Directory of Open Access Books |
| description | 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. Programmsynthese ist die automatische Konstruktion eines Computerprogramms, das eine gegebene formale Spezifikation erfüllt. Anders als herkömmliche Verfahren zur Programmkonstruktion wie Übersetzer, kann Programmsynthese Programme erzeugen, die nicht nur durch rein syntaktische Transformationen aus der Spezifikation abgeleitet werden können. Diese Fähigkeit ist essenziell für die Erzeugung effizienter Programme für spezialisierte Hardware mit eingeschränktem Instruktionssatz oder um Spezifikationen wie Eingabe-Ausgabe-Beispiele nutzen zu können. Leider begrenzt der große Suchraum möglicher Programme die Skalierbarkeit der Programmsynthese in der Praxis. Diese Dissertation stellt Techniken vor, um die Programmsynthese schleifenfreier Bitvektor-Programme, die für eine nutzerdefinierte Metrik optimal sind, zu beschleunigen. Bitvektor-Programme verarbeiten Daten fester Bitbreite. Die vorgestellten Techniken stellen approximativ fest, ob ein Programmsyntheseproblem unlösbar ist, das heißt, ob die gegebenen Operationen ausreichen, um daraus ein Programm zu konstruieren, das die Spezifikation implementiert. Dazu untersucht diese Dissertation Ansätze, um die Abhängigkeiten zwischen Eingabe- und Ausgabe-Bits der Spezifikation zu bestimmen und dieses Wissen für die Analyse von Programmsyntheseproblemen einzusetzen. Eine Auswertung der vorgestellten Techniken zeigt, dass sie die notwendige Zeit zur Synthese optimaler Bitvektor-Programme deutlich reduzieren können. |
| format | Online |
| id | doab-20.500.12854ir-170195 |
| institution | Directory of Open Access Books |
| language | eng |
| publishDate | 2025 |
| publishDateRange | 2025 |
| publishDateSort | 2025 |
| publisher | FAU University Press |
| publisherStr | FAU University Press |
| record_format | ojs |
| spelling | doab-20.500.12854ir-1701952025-12-16T05:17:14Z Detecting Unrealizable Bit Vector Program Synthesis Problems Kamp, Marius boolesche Funktion Bitvektor Algorithmus Programmsynthese thema EDItEUR::U Computing and Information Technology::UM Computer programming / software engineering::UMC Compilers and interpreters thema EDItEUR::U Computing and Information Technology::UY Computer science::UYA Mathematical theory of computation 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. Programmsynthese ist die automatische Konstruktion eines Computerprogramms, das eine gegebene formale Spezifikation erfüllt. Anders als herkömmliche Verfahren zur Programmkonstruktion wie Übersetzer, kann Programmsynthese Programme erzeugen, die nicht nur durch rein syntaktische Transformationen aus der Spezifikation abgeleitet werden können. Diese Fähigkeit ist essenziell für die Erzeugung effizienter Programme für spezialisierte Hardware mit eingeschränktem Instruktionssatz oder um Spezifikationen wie Eingabe-Ausgabe-Beispiele nutzen zu können. Leider begrenzt der große Suchraum möglicher Programme die Skalierbarkeit der Programmsynthese in der Praxis. Diese Dissertation stellt Techniken vor, um die Programmsynthese schleifenfreier Bitvektor-Programme, die für eine nutzerdefinierte Metrik optimal sind, zu beschleunigen. Bitvektor-Programme verarbeiten Daten fester Bitbreite. Die vorgestellten Techniken stellen approximativ fest, ob ein Programmsyntheseproblem unlösbar ist, das heißt, ob die gegebenen Operationen ausreichen, um daraus ein Programm zu konstruieren, das die Spezifikation implementiert. Dazu untersucht diese Dissertation Ansätze, um die Abhängigkeiten zwischen Eingabe- und Ausgabe-Bits der Spezifikation zu bestimmen und dieses Wissen für die Analyse von Programmsyntheseproblemen einzusetzen. Eine Auswertung der vorgestellten Techniken zeigt, dass sie die notwendige Zeit zur Synthese optimaler Bitvektor-Programme deutlich reduzieren können. 2025-12-16T05:17:13Z 2025-12-16T05:17:13Z 2025-12-15T15:08:58Z 2025 book ONIX_20251215T160703_9783961477944_9 https://library.oapen.org/handle/20.500.12657/109178 9783961477944 9783961477937 https://directory.doabooks.org/handle/20.500.12854/170195 eng FAU Studien aus der Informatik open access image/jpeg Attribution 4.0 International https://library.oapen.org/bitstream/20.500.12657/109178/1/9783961477944.pdf FAU University Press 10.25593/978-3-96147-794-4 10.25593/978-3-96147-794-4 2c600dea-eece-4066-87be-da335e323fdb 9783961477944 9783961477937 261 Erlangen open access |
| spellingShingle | boolesche Funktion Bitvektor Algorithmus Programmsynthese thema EDItEUR::U Computing and Information Technology::UM Computer programming / software engineering::UMC Compilers and interpreters thema EDItEUR::U Computing and Information Technology::UY Computer science::UYA Mathematical theory of computation Kamp, Marius Detecting Unrealizable Bit Vector Program Synthesis Problems |
| title | Detecting Unrealizable Bit Vector Program Synthesis Problems |
| title_full | Detecting Unrealizable Bit Vector Program Synthesis Problems |
| title_fullStr | Detecting Unrealizable Bit Vector Program Synthesis Problems |
| title_full_unstemmed | Detecting Unrealizable Bit Vector Program Synthesis Problems |
| title_short | Detecting Unrealizable Bit Vector Program Synthesis Problems |
| title_sort | detecting unrealizable bit vector program synthesis problems |
| topic | boolesche Funktion Bitvektor Algorithmus Programmsynthese thema EDItEUR::U Computing and Information Technology::UM Computer programming / software engineering::UMC Compilers and interpreters thema EDItEUR::U Computing and Information Technology::UY Computer science::UYA Mathematical theory of computation |
| topic_facet | boolesche Funktion Bitvektor Algorithmus Programmsynthese thema EDItEUR::U Computing and Information Technology::UM Computer programming / software engineering::UMC Compilers and interpreters thema EDItEUR::U Computing and Information Technology::UY Computer science::UYA Mathematical theory of computation |
| url | ONIX_20251215T160703_9783961477944_9 |
| work_keys_str_mv | AT kampmarius detectingunrealizablebitvectorprogramsynthesisproblems |