Towards synthesis from assume-guarantee contracts involving infinite theories
Andreas Katis, Andrew Gacek, Michael W. Whalen · 2016
In previous work, we have introduced a contract-based realizability checking algorithm for assume-guarantee contracts involving infinite theories, such as linear integer/real arithmetic and uninterpreted functions over infinite domains. This algorithm can determine whether or not it is possible to construct a realization (i.e. an implementation) of an assumeguarantee contract. The algorithm is similar to k-induction model checking, but involves the use of quantifiers to determine implementability.