Towards synthesis from assume-guarantee contracts involving infinite theories: A preliminary report

Andreas Katis, Andrew Gacek, Michael W. Whalen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

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 assume-guarantee contract. The algorithm is similar to k-induction model checking, but involves the use of quantifiers to determine implementability. While our work on realizability is inherently useful for virtual integration in determining whether it is possible for suppliers 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 involving infinite theories. To do so, we take advantage of our realizability checking procedure and a skolemization solver for ∀∃-formulas, called AE-VAL. We show that it is possible to immediately adapt our existing algorithm towards synthesis by using this solver, using a demonstration example. We then discuss challenges towards creating a more robust synthesis algorithm.

Original languageEnglish (US)
Title of host publicationProceedings - 4th FME Workshop on Formal Methods in Software Engineering, FormaliSE 2016
PublisherAssociation for Computing Machinery, Inc
Pages36-41
Number of pages6
ISBN (Electronic)9781450341592
DOIs
StatePublished - May 14 2016
Event4th FME Workshop on Formal Methods in Software Engineering, FormaliSE 2016 - Austin, United States
Duration: May 15 2016 → …

Publication series

NameProceedings - 4th FME Workshop on Formal Methods in Software Engineering, FormaliSE 2016

Conference

Conference4th FME Workshop on Formal Methods in Software Engineering, FormaliSE 2016
CountryUnited States
CityAustin
Period5/15/16 → …

Fingerprint Dive into the research topics of 'Towards synthesis from assume-guarantee contracts involving infinite theories: A preliminary report'. Together they form a unique fingerprint.

  • Cite this

    Katis, A., Gacek, A., & Whalen, M. W. (2016). Towards synthesis from assume-guarantee contracts involving infinite theories: A preliminary report. In Proceedings - 4th FME Workshop on Formal Methods in Software Engineering, FormaliSE 2016 (pp. 36-41). (Proceedings - 4th FME Workshop on Formal Methods in Software Engineering, FormaliSE 2016). Association for Computing Machinery, Inc. https://doi.org/10.1145/2897667.2897675