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)

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 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
Pages92-110
ISBN (Electronic)978-3-319-57666-4
DOIs
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
PublisherSpringer
Volume10231
ISSN (Electronic)1611-3349

Workshop

WorkshopInternational Workshop on Formal Aspects of Component Software
Abbreviated titleFACS
CountryFrance
CityBesançon
Period19/10/201621/10/2016

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). https://doi.org/10.1007/978-3-319-57666-4_7