Constrained Synthesis from Component Libraries

Antonio Iannopollo, Stavros Tripakis, Alberto Sangiovanni-Vincentelli

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

3 Citations (Scopus)


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 an industrial case study.
Original languageEnglish
Title of host publicationFormal Aspects of Component Software
Subtitle of host publication13th International Conference, FACS 2016, Besançon, France, October 19-21, 2016, Revised Selected Papers
ISBN (Electronic)978-3-319-57666-4
Publication statusPublished - 2017
MoE publication typeA4 Article in a conference publication
EventInternational Workshop on Formal Aspects of Component Software - Besançon, France
Duration: 19 Oct 201621 Oct 2016
Conference number: 13

Publication series

NameLecture Notes in Computer Science
ISSN (Electronic)1611-3349


WorkshopInternational Workshop on Formal Aspects of Component Software
Abbreviated titleFACS

Fingerprint Dive into the research topics of 'Constrained Synthesis from Component Libraries'. Together they form a unique fingerprint.

  • Cite this

    Iannopollo, A., Tripakis, S., & Sangiovanni-Vincentelli, A. (2017). Constrained Synthesis from Component Libraries. In Formal Aspects of Component Software: 13th International Conference, FACS 2016, Besançon, France, October 19-21, 2016, Revised Selected Papers (pp. 92-110). (Lecture Notes in Computer Science ; Vol. 10231).