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

TL;DR

This paper introduces a preliminary synthesis algorithm for assume-guarantee contracts involving infinite theories, building on prior realizability checking methods and leveraging a Skolemization solver to enable component synthesis.

Contribution

It extends previous realizability algorithms to support synthesis of implementations from assume-guarantee contracts with infinite theories using AE-VAL solver.

Findings

Demonstrates initial synthesis approach with an example

Adapts realizability checking for synthesis tasks

Discusses challenges for robust synthesis algorithms

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.