Constrained synthesis from component libraries

Research output: Contribution to journalArticleScientificpeer-review

Details

Original languageEnglish
Pages (from-to)21-41
Number of pages21
JournalScience of Computer Programming
Volume171
StatePublished - 15 Feb 2019
MoE publication typeA1 Journal article-refereed

Researchers

Research units

  • University of California at Berkeley
  • Northeastern University

Abstract

Synthesis from component libraries is the problem of building a network of components from a given library, such that the network realizes a given specification. This problem is undecidable in general. It becomes decidable if we impose a bound on the number of chosen components. However, the bounded problem remains computationally hard and brute-force approaches do not scale. In this paper, we study scalable methods for solving the problem of bounded synthesis from libraries, proposing a solution based on the Counterexample-Guided Inductive Synthesis paradigm. Although our synthesis algorithm does not assume a specific formalism a priori, we present a parallel implementation which instantiates components defined as Linear Temporal Logic-based Assume/Guarantee Contracts. We show the potential of our approach and evaluate our implementation by applying it to two industrial-relevant case studies.

    Research areas

  • Assume-guarantee contracts, Component libraries, Counterexample-guided inductive synthesis, Linear temporal logic, Platform-based design

ID: 30129275