(2018) Bounded Synthesis of Reactive Programs.
Abstract
Most algorithms for the synthesis of reactive systems focus on the construction of finite-state machines rather than actual programs. This often leads to badly structured, unreadable code. In this paper, we present a bounded synthesis approach that automatically constructs, from a given specification in linear-time temporal logic (LTL), a program in Madhusudan's simple imperative language for reactive programs. We develop and compare two principal approaches for the reduction of the synthesis problem to a Boolean constraint satisfaction problem. The first reduction is based on a generalization of bounded synthesis to two-way alternating automata, the second reduction is based on a direct encoding of the program syntax in the constraint system. We report on preliminary experience with a prototype implementation, which indicates that the direct encoding outperforms the automata approach.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Conference: | ATVA International Symposium on Automated Technology for Verification and Analysis |
| Depositing User: | Bernd Finkbeiner |
| Date Deposited: | 23 Jun 2019 18:39 |
| Last Modified: | 14 Oct 2020 13:01 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/2927 |
Actions
Actions (login required)
 |
View Item |