### 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.

Original language | English |
---|---|

Pages (from-to) | 21-41 |

Number of pages | 21 |

Journal | Science of Computer Programming |

Volume | 171 |

DOIs | |

Publication status | Published - 15 Feb 2019 |

MoE publication type | A1 Journal article-refereed |

### Keywords

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

## Fingerprint Dive into the research topics of 'Constrained synthesis from component libraries'. Together they form a unique fingerprint.

## Cite this

*Science of Computer Programming*,

*171*, 21-41. https://doi.org/10.1016/j.scico.2018.10.003