|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'504'928
Articles rated: 2609
25 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report | | Andreas Katis
; Michael W. Whalen
; Andrew Gacek
; | | Date: |
30 Jan 2016 | | Abstract: | In previous work, we have introduced a contract-based real- izability
checking algorithm for assume-guarantee contracts involving infinite theories,
such as linear integer/real arith- metic and uninterpreted functions over
infinite domains. This algorithm can determine whether or not it is possible to
con- struct a realization (i.e. an implementation) of an assume- guarantee
contract. The algorithm is similar to k-induction model checking, but involves
the use of quantifiers to deter- mine implementability. While our work on
realizability is inherently useful for vir- tual integration in determining
whether it is possible for sup- pliers to build software that meets a contract,
it also provides the foundations to solving the more challenging problem of
component synthesis. In this paper, we provide an initial synthesis algorithm
for assume-guarantee contracts involv- ing infinite theories. To do so, we take
advantage of our realizability checking procedure and a skolemization solver
for forall-exists formulas, called AE-VAL. We show that it is possible to
immediately adapt our existing algorithm towards syn- thesis by using this
solver, using a demonstration example. We then discuss challenges towards
creating a more robust synthesis algorithm. | | Source: | arXiv, 1602.0148 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER