ML p(r)ior | Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report

Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report

2016-01-30
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.
PDF

Highlights - Most important sentences from the article

Login to like/save this paper, take notes and configure your recommendations

Related Articles

2017-12-01

Reactive systems that operate in environments with complex data, such as mobile apps or embedded con… show more
PDF

Highlights - Most important sentences from the article

2018-10-12

This paper introduces assume/guarantee contracts on continuous-time control systems, hereby extendin… show more
PDF

Highlights - Most important sentences from the article

2019-03-28

We prove that certain formulations of program synthesis and reachability are equivalent. Specificall… show more
PDF

Highlights - Most important sentences from the article

2019-03-22
1903.09475 | cs.AI

Artificial Intelligence problems, ranging form planning/scheduling up to game control, include an es… show more
PDF

Highlights - Most important sentences from the article

2016-11-23
1611.07803 | cs.LO

This paper considers the problem of assumptions refinement in the context of unrealizable specificat… show more
PDF

Highlights - Most important sentences from the article

2019-03-27

Dynamic model inference techniques have been the center of many research projects recently. There ar… show more
PDF

Highlights - Most important sentences from the article

2018-12-03
1812.00619 | cs.LO

Smart contracts are a special type of programs running inside a blockchain. Immutable and transparen… show more
PDF

Highlights - Most important sentences from the article

2018-07-24

Most algorithms for the synthesis of reactive systems focus on the construction of finite-state mach… show more
PDF

Highlights - Most important sentences from the article

2019-01-03
1901.00591 | cs.LO

In formal synthesis of reactive systems an implementation of a system is automatically constructed f… show more
PDF

Highlights - Most important sentences from the article

2018-08-28
1808.09430 | cs.LO

Reactive synthesis is an automatic way to translate a human intention expressed in some logic into a… show more
PDF

Highlights - Most important sentences from the article

2018-09-23
1809.08576 | cs.LO

We present an approach for proving the correctness of distributed algorithms that obviate interleavi… show more
PDF

Highlights - Most important sentences from the article

2019-06-07
1906.02906 | cs.SE

Modern blockchain systems support creation of smart contracts -- stateful programs hosted and execut… show more
PDF

Highlights - Most important sentences from the article

2017-12-15

We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfia… show more
PDF

Highlights - Most important sentences from the article

2014-11-03

#SMT, or model counting for logical theories, is a well-known hard problem that generalizes such tas… show more
PDF

Highlights - Most important sentences from the article

2017-04-11

This paper describes three variants of a counterexample guided inductive optimization (CEGIO) approa… show more
PDF

Highlights - Most important sentences from the article

2017-05-23

LTLf synthesis is the process of finding a strategy that satisfies a linear temporal specification o… show more
PDF

Highlights - Most important sentences from the article